Theorem nfra1 3222

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

Syntax hints:   → wi 4  ∀wal 1534  Ⅎwnf 1783   ∈ wcel 2113  ∀wral 3141

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 2144

This theorem depends on definitions:  df-bi 209  df-or 844  df-ex 1780  df-nf 1784  df-ral 3146

This theorem is referenced by:  hbra1  3223  nfra2w  3230  nfra2  3231  ralbiOLD  3236  ralrexbidOLD  3326  r19.12  3327  r19.12OLD  3330  ralcom2  3366  2reu1  3884  nfss  3963  rspn0  4316  ralidm  4458  2reu4lem  4468  iuneqconst  4933  nfii1  4957  dfiun2g  4958  dfiun2gOLD  4959  mpteq12f  5152  reusv1  5301  reusv2lem1  5302  reusv2lem2  5303  reusv2lem3  5304  ralxfrALT  5319  fvmptss  6783  ffnfv  6885  riota5f  7145  mpoeq123  7229  tfinds  7577  peano5  7608  zfrep6  7659  wfrlem4  7961  tfr3  8038  tz7.48-1  8082  tz7.49  8084  nfixp1  8485  nneneq  8703  scottex  9317  dfac2b  9559  infpssrlem4  9731  hsmexlem2  9852  hsmexlem4  9854  domtriomlem  9867  axdc3lem2  9876  axdc3lem4  9878  axdc4lem  9880  zorn2lem5  9925  konigthlem  9993  eltsk2g  10176  dedekind  10806  dedekindle  10807  lble  11596  fsuppmapnn0fiublem  13361  fsuppmapnn0fiub  13362  fsuppmapnn0fiubex  13363  prodeq2ii  15270  fprodle  15353  lcmfunsnlem1  15984  lcmfunsnlem2lem1  15985  lcmfunsnlem2  15987  mreiincl  16870  mreexexd  16922  catpropd  16982  acsmapd  17791  gsummatr01lem4  21270  cpmatmcllem  21329  alexsubALTlem3  22660  isucn2  22891  mptelee  26684  chirred  30175  opreu2reuALT  30243  foresf1o  30268  abrexss  30275  aciunf1lem  30410  nn0min  30540  fprodex01  30545  isarchiofld  30894  reff  31107  locfinreflem  31108  cmpcref  31118  esumcl  31293  measvunilem  31475  measvunilem0  31476  measvuni  31477  voliune  31492  volfiniune  31493  omssubadd  31562  bnj1366  32105  bnj1379  32106  bnj571  32182  bnj1039  32247  bnj1128  32266  bnj1204  32288  bnj1279  32294  bnj1307  32299  bnj1388  32309  bnj1398  32310  bnj1444  32319  bnj1489  32332  bnj1525  32345  dfon2lem3  33034  trpredmintr  33074  frrlem4  33130  nosupbnd1  33218  domalom  34689  ralssiun  34692  fvineqsneu  34696  fvineqsneq  34697  heicant  34931  cover2  34993  upixp  35008  indexdom  35013  filbcmb  35019  riotasvd  36096  riotasv2d  36097  riotasv2s  36098  glbconxN  36518  pmapglbx  36909  pmapglb2xN  36912  cdleme26ee  37500  cdlemefr29exN  37542  cdlemefs32sn1aw  37554  cdleme43fsv1snlem  37560  cdleme41sn3a  37573  cdleme32d  37584  cdleme32f  37586  cdleme40m  37607  cdleme40n  37608  cdlemk36  38053  cdlemk38  38055  cdlemkid  38076  cdlemk19x  38083  cdlemk11t  38086  mzpexpmpt  39348  gneispace  40490  mnuprdlem4  40617  ssralv2  40871  tratrb  40876  fnchoice  41292  rfcnnnub  41299  uzwo4  41321  ralimralim  41351  ralimda  41412  suprnmpt  41436  fompt  41459  choicefi  41469  axccdom  41493  axccd  41501  rnmptlb  41520  rnmptbddlem  41521  rnmptbd2lem  41526  rnmptbdlem  41533  upbdrech  41578  ssfiunibd  41582  iuneqfzuzlem  41608  infxrunb2  41642  xrralrecnnle  41659  supxrunb3  41678  supxrleubrnmpt  41685  unb2ltle  41695  rexabslelem  41698  allbutfiinf  41700  suprleubrnmpt  41702  uzub  41711  infxrgelbrnmpt  41736  mccl  41885  climsuse  41895  mullimc  41903  islptre  41906  mullimcf  41910  limcrecl  41916  islpcn  41926  limsupre  41928  limcleqr  41931  addlimc  41935  0ellimcdiv  41936  limclner  41938  climinf2lem  41993  limsupubuz  42000  climinf3  42003  limsupmnflem  42007  limsupmnfuzlem  42013  limsupre3uzlem  42022  climisp  42033  climrescn  42035  climxrrelem  42036  climxrre  42037  xlimmnfv  42121  xlimpnfv  42125  climxlim2lem  42132  cncfioobd  42186  stoweidlem16  42308  stoweidlem28  42320  stoweidlem29  42321  stoweidlem31  42323  stoweidlem35  42327  stoweidlem48  42340  stoweidlem51  42343  stoweidlem52  42344  stoweidlem53  42345  stoweidlem54  42346  stoweidlem56  42348  stoweidlem57  42349  stoweidlem59  42351  stoweidlem60  42352  stoweidlem62  42354  wallispilem3  42359  stirlinglem13  42378  fourierdlem31  42430  fourierdlem39  42438  fourierdlem68  42466  fourierdlem71  42469  fourierdlem73  42471  fourierdlem77  42475  fourierdlem83  42481  fourierdlem87  42485  fourierdlem94  42492  fourierdlem103  42501  fourierdlem104  42502  fourierdlem112  42510  fourierdlem113  42511  salexct  42624  subsaliuncl  42648  sge0lefi  42687  sge0isum  42716  sge0reuzb  42737  iundjiun  42749  voliunsge0lem  42761  meaiuninc3v  42773  ovnsubaddlem2  42860  hoiqssbllem3  42913  vonioo  42971  vonicc  42974  preimageiingt  43005  preimaleiinlt  43006  issmfle  43029  issmfgt  43040  issmfge  43053  smflimlem2  43055  smfsupmpt  43096  smfinflem  43098  smfinfmpt  43100  smfliminflem  43111  ffnafv  43377  iccelpart  43600  sprsymrelfo  43666  mogoldbb  43957  sbgoldbo  43959  iunord  44786  setrec1lem2  44798  aacllem  44909