Theorem nfra1 3284

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 3062	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		nfa1 2151	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	nfxfr 1853	1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783   ∈ wcel 2108  ∀wral 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-or 849  df-ex 1780  df-nf 1784  df-ral 3062

This theorem is referenced by:  hbra1  3301  r19.12  3314  r19.12OLD  3315  nfra2  3376  ralcom2  3377  2reu1  3897  nfss  3976  2reu4lem  4522  iuneqconst  5003  nfii1  5029  dfiun2gOLD  5031  mpteq12f  5230  reusv1  5397  reusv2lem1  5398  reusv2lem2  5399  reusv2lem3  5400  ralxfrALT  5415  fvmptss  7028  fompt  7138  ffnfv  7139  riota5f  7416  mpoeq123  7505  tfinds  7881  zfrep6  7979  frrlem4  8314  wfrlem4OLD  8352  tfr3  8439  tz7.48-1  8483  tz7.49  8485  naddsuc2  8739  nfixp1  8958  nneneq  9246  nneneqOLD  9258  scottex  9925  dfac2b  10171  infpssrlem4  10346  hsmexlem2  10467  hsmexlem4  10469  domtriomlem  10482  axdc3lem2  10491  axdc3lem4  10493  axdc4lem  10495  zorn2lem5  10540  konigthlem  10608  eltsk2g  10791  dedekind  11424  dedekindle  11425  lble  12220  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  fsuppmapnn0fiubex  14033  prodeq2ii  15947  fprodle  16032  lcmfunsnlem1  16674  lcmfunsnlem2lem1  16675  lcmfunsnlem2  16677  mreiincl  17639  mreexexd  17691  catpropd  17752  acsmapd  18599  gsummatr01lem4  22664  cpmatmcllem  22724  alexsubALTlem3  24057  isucn2  24288  nosupbnd1  27759  noinfbnd1  27774  mptelee  28910  chirred  32414  opreu2reuALT  32496  foresf1o  32523  abrexss  32531  iinabrex  32582  aciunf1lem  32672  nn0min  32822  fprodex01  32827  isarchiofld  33347  elrspunidl  33456  reff  33838  locfinreflem  33839  cmpcref  33849  zarcmplem  33880  esumcl  34031  measvunilem  34213  measvunilem0  34214  measvuni  34215  voliune  34230  volfiniune  34231  omssubadd  34302  bnj1366  34843  bnj1379  34844  bnj571  34920  bnj1039  34985  bnj1128  35004  bnj1204  35026  bnj1279  35032  bnj1307  35037  bnj1388  35047  bnj1398  35048  bnj1444  35057  bnj1489  35070  bnj1525  35083  dfon2lem3  35786  domalom  37405  ralssiun  37408  fvineqsneu  37412  fvineqsneq  37413  heicant  37662  cover2  37722  upixp  37736  indexdom  37741  filbcmb  37747  riotasvd  38957  riotasv2d  38958  riotasv2s  38959  glbconxN  39380  pmapglbx  39771  pmapglb2xN  39774  cdleme26ee  40362  cdlemefr29exN  40404  cdlemefs32sn1aw  40416  cdleme43fsv1snlem  40422  cdleme41sn3a  40435  cdleme32d  40446  cdleme32f  40448  cdleme40m  40469  cdleme40n  40470  cdlemk36  40915  cdlemk38  40917  cdlemkid  40938  cdlemk19x  40945  cdlemk11t  40948  mzpexpmpt  42756  nadd1suc  43405  gneispace  44147  mnuprdlem4  44294  ssralv2  44551  tratrb  44556  modelaxrep  44998  fnchoice  45034  rfcnnnub  45041  uzwo4  45058  ralimralim  45086  suprnmpt  45179  choicefi  45205  axccdom  45227  axccd  45234  rnmptlb  45250  rnmptbddlem  45251  rnmptbd2lem  45255  rnmptbdlem  45262  upbdrech  45317  ssfiunibd  45321  iuneqfzuzlem  45345  infxrunb2  45379  xrralrecnnle  45394  supxrunb3  45410  supxrleubrnmpt  45417  unb2ltle  45426  rexabslelem  45429  allbutfiinf  45431  suprleubrnmpt  45433  uzub  45442  infxrgelbrnmpt  45465  cvgcaule  45502  mccl  45613  climsuse  45623  mullimc  45631  islptre  45634  mullimcf  45638  limcrecl  45644  islpcn  45654  limsupre  45656  limcleqr  45659  addlimc  45663  0ellimcdiv  45664  limclner  45666  climinf2lem  45721  limsupubuz  45728  climinf3  45731  limsupmnflem  45735  limsupmnfuzlem  45741  limsupre3uzlem  45750  climisp  45761  climrescn  45763  climxrrelem  45764  climxrre  45765  xlimmnfv  45849  xlimpnfv  45853  climxlim2lem  45860  cncfioobd  45912  stoweidlem16  46031  stoweidlem28  46043  stoweidlem29  46044  stoweidlem31  46046  stoweidlem35  46050  stoweidlem48  46063  stoweidlem51  46066  stoweidlem52  46067  stoweidlem53  46068  stoweidlem54  46069  stoweidlem56  46071  stoweidlem57  46072  stoweidlem59  46074  stoweidlem60  46075  stoweidlem62  46077  wallispilem3  46082  stirlinglem13  46101  fourierdlem31  46153  fourierdlem39  46161  fourierdlem68  46189  fourierdlem71  46192  fourierdlem73  46194  fourierdlem77  46198  fourierdlem83  46204  fourierdlem87  46208  fourierdlem94  46215  fourierdlem103  46224  fourierdlem104  46225  fourierdlem112  46233  fourierdlem113  46234  salexct  46349  subsaliuncl  46373  sge0lefi  46413  sge0isum  46442  sge0reuzb  46463  iundjiun  46475  voliunsge0lem  46487  meaiuninc3v  46499  ovnsubaddlem2  46586  hoiqssbllem3  46639  vonioo  46697  vonicc  46700  preimageiingt  46735  preimaleiinlt  46736  issmfle  46760  issmfgt  46771  issmfge  46785  smflimlem2  46787  smfsupmpt  46830  smfinflem  46832  smfinfmpt  46834  smfliminflem  46845  fsupdm  46857  finfdm  46861  ffnafv  47183  iccelpart  47420  sprsymrelfo  47484  mogoldbb  47772  sbgoldbo  47774  iunord  49195  setrec1lem2  49207  pgind  49236  aacllem  49320