Theorem nfra1 2925

Description: The setvar 𝑥 is not free in ∀𝑥 ∈ 𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfra1	⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Proof of Theorem nfra1

Step	Hyp	Ref	Expression
1		df-ral 2901	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		nfa1 2015	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	nfxfr 1771	1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4  ∀wal 1473  Ⅎwnf 1699   ∈ wcel 1977  ∀wral 2896

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-10 2006

This theorem depends on definitions:  df-bi 196  df-or 384  df-ex 1696  df-nf 1701  df-ral 2901

This theorem is referenced by:  hbra1  2926  nfra2  2930  r19.12  3045  ralbi  3050  ralcom2  3083  nfss  3561  rspn0  3892  ralidm  4027  nfii1  4487  dfiun2g  4488  mpteq12f  4661  reusv1  4792  reusv1OLD  4793  reusv2lem1  4794  reusv2lem2  4795  reusv2lem2OLD  4796  reusv2lem3  4797  ralxfrALT  4813  fvmptss  6201  ffnfv  6295  riota5f  6535  mpt2eq123  6612  tfinds  6951  peano5  6981  fun11iun  7019  zfrep6  7027  wfrlem4  7305  tfr3  7382  tz7.48-1  7425  tz7.49  7427  nfixp1  7814  nneneq  8028  scottex  8631  dfac2  8836  infpssrlem4  9011  hsmexlem2  9132  hsmexlem4  9134  domtriomlem  9147  axdc3lem2  9156  axdc3lem4  9158  axdc4lem  9160  zorn2lem5  9205  konigthlem  9269  eltsk2g  9452  dedekind  10079  dedekindle  10080  lble  10854  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  fsuppmapnn0fiubex  12654  prodeq2ii  14482  fprodle  14566  lcmfunsnlem1  15188  lcmfunsnlem2lem1  15189  lcmfunsnlem2  15191  mreiincl  16079  mreexexd  16131  mreexexdOLD  16132  catpropd  16192  acsmapd  17001  gsummatr01lem4  20283  cpmatmcllem  20342  pmatcollpwfi  20406  alexsubALTlem3  21663  isucn2  21893  mptelee  25575  chirred  28638  foresf1o  28727  abrexss  28734  aciunf1lem  28844  nn0min  28954  isarchiofld  29148  reff  29234  locfinreflem  29235  cmpcref  29245  esumcl  29419  measvunilem  29602  measvunilem0  29603  measvuni  29604  voliune  29619  volfiniune  29620  omssubadd  29689  bnj1366  30154  bnj1379  30155  bnj571  30230  bnj1039  30293  bnj1128  30312  bnj1204  30334  bnj1279  30340  bnj1307  30345  bnj1388  30355  bnj1398  30356  bnj1444  30365  bnj1489  30378  bnj1525  30391  dfon2lem3  30934  trpredmintr  30975  frrlem4  31027  heicant  32614  cover2  32678  upixp  32694  indexdom  32699  filbcmb  32705  riotasvd  33260  riotasv2d  33261  riotasv2s  33262  glbconxN  33682  pmapglbx  34073  pmapglb2xN  34076  cdleme26ee  34666  cdlemefr29exN  34708  cdlemefs32sn1aw  34720  cdleme43fsv1snlem  34726  cdleme41sn3a  34739  cdleme32d  34750  cdleme32f  34752  cdleme40m  34773  cdleme40n  34774  cdlemk36  35219  cdlemk38  35221  cdlemkid  35242  cdlemk19x  35249  cdlemk11t  35252  mzpexpmpt  36326  gneispace  37452  ssralv2  37758  tratrb  37767  fnchoice  38211  rfcnnnub  38218  uzwo4  38246  ralimralim  38279  suprnmpt  38350  fompt  38374  choicefi  38387  axccdom  38411  axccd  38424  upbdrech  38460  ssfiunibd  38464  iuneqfzuzlem  38491  infxrunb2  38525  xrralrecnnle  38543  mccl  38665  climsuse  38675  mullimc  38683  islptre  38686  mullimcf  38690  limcrecl  38696  islpcn  38706  limsupre  38708  limcleqr  38711  addlimc  38715  0ellimcdiv  38716  limclner  38718  cncfioobd  38783  stoweidlem16  38909  stoweidlem28  38921  stoweidlem29  38922  stoweidlem31  38924  stoweidlem35  38928  stoweidlem48  38941  stoweidlem51  38944  stoweidlem52  38945  stoweidlem53  38946  stoweidlem54  38947  stoweidlem56  38949  stoweidlem57  38950  stoweidlem59  38952  stoweidlem60  38953  stoweidlem62  38955  wallispilem3  38960  stirlinglem13  38979  fourierdlem31  39031  fourierdlem39  39039  fourierdlem68  39067  fourierdlem71  39070  fourierdlem73  39072  fourierdlem77  39076  fourierdlem83  39082  fourierdlem87  39086  fourierdlem94  39093  fourierdlem103  39102  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  salexct  39228  subsaliuncl  39252  sge0lefi  39291  sge0isum  39320  sge0reuzb  39341  iundjiun  39353  voliunsge0lem  39365  ovnsubaddlem2  39461  hoiqssbllem3  39514  vonioo  39573  vonicc  39576  preimageiingt  39607  preimaleiinlt  39608  issmfle  39632  issmfgt  39643  issmfge  39656  smflimlem2  39658  2reu1  39835  2reu4a  39838  ffnafv  39900  iccelpart  39971  iunord  42220  setrec1lem2  42234  aacllem  42356