Theorem nfra1 3262

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3045

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 2142

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

This theorem is referenced by:  hbra1  3277  r19.12  3290  nfra2  3352  ralcom2  3353  2reu1  3863  nfss  3942  2reu4lem  4488  iuneqconst  4970  nfii1  4996  dfiun2gOLD  4998  mpteq12f  5195  reusv1  5355  reusv2lem1  5356  reusv2lem2  5357  reusv2lem3  5358  ralxfrALT  5373  fvmptss  6983  fompt  7093  ffnfv  7094  riota5f  7375  mpoeq123  7464  tfinds  7839  zfrep6  7936  frrlem4  8271  tfr3  8370  tz7.48-1  8414  tz7.49  8416  naddsuc2  8668  nfixp1  8894  nneneq  9176  scottex  9845  dfac2b  10091  infpssrlem4  10266  hsmexlem2  10387  hsmexlem4  10389  domtriomlem  10402  axdc3lem2  10411  axdc3lem4  10413  axdc4lem  10415  zorn2lem5  10460  konigthlem  10528  eltsk2g  10711  dedekind  11344  dedekindle  11345  lble  12142  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  fsuppmapnn0fiubex  13964  prodeq2ii  15884  fprodle  15969  lcmfunsnlem1  16614  lcmfunsnlem2lem1  16615  lcmfunsnlem2  16617  mreiincl  17564  mreexexd  17616  catpropd  17677  acsmapd  18520  gsummatr01lem4  22552  cpmatmcllem  22612  alexsubALTlem3  23943  isucn2  24173  nosupbnd1  27633  noinfbnd1  27648  mptelee  28829  chirred  32331  opreu2reuALT  32413  foresf1o  32440  abrexss  32448  iinabrex  32505  aciunf1lem  32593  nn0min  32752  fprodex01  32757  isarchiofld  33302  elrspunidl  33406  reff  33836  locfinreflem  33837  cmpcref  33847  zarcmplem  33878  esumcl  34027  measvunilem  34209  measvunilem0  34210  measvuni  34211  voliune  34226  volfiniune  34227  omssubadd  34298  bnj1366  34826  bnj1379  34827  bnj571  34903  bnj1039  34968  bnj1128  34987  bnj1204  35009  bnj1279  35015  bnj1307  35020  bnj1388  35030  bnj1398  35031  bnj1444  35040  bnj1489  35053  bnj1525  35066  dfon2lem3  35780  domalom  37399  ralssiun  37402  fvineqsneu  37406  fvineqsneq  37407  heicant  37656  cover2  37716  upixp  37730  indexdom  37735  filbcmb  37741  riotasvd  38956  riotasv2d  38957  riotasv2s  38958  glbconxN  39379  pmapglbx  39770  pmapglb2xN  39773  cdleme26ee  40361  cdlemefr29exN  40403  cdlemefs32sn1aw  40415  cdleme43fsv1snlem  40421  cdleme41sn3a  40434  cdleme32d  40445  cdleme32f  40447  cdleme40m  40468  cdleme40n  40469  cdlemk36  40914  cdlemk38  40916  cdlemkid  40937  cdlemk19x  40944  cdlemk11t  40947  mzpexpmpt  42740  nadd1suc  43388  gneispace  44130  mnuprdlem4  44271  ssralv2  44528  tratrb  44533  modelaxrep  44978  fnchoice  45030  rfcnnnub  45037  uzwo4  45054  ralimralim  45082  suprnmpt  45175  choicefi  45201  axccdom  45223  axccd  45230  rnmptlb  45244  rnmptbddlem  45245  rnmptbd2lem  45249  rnmptbdlem  45256  upbdrech  45310  ssfiunibd  45314  iuneqfzuzlem  45337  infxrunb2  45371  xrralrecnnle  45386  supxrunb3  45402  supxrleubrnmpt  45409  unb2ltle  45418  rexabslelem  45421  allbutfiinf  45423  suprleubrnmpt  45425  uzub  45434  infxrgelbrnmpt  45457  cvgcaule  45494  mccl  45603  climsuse  45613  mullimc  45621  islptre  45624  mullimcf  45628  limcrecl  45634  islpcn  45644  limsupre  45646  limcleqr  45649  addlimc  45653  0ellimcdiv  45654  limclner  45656  climinf2lem  45711  limsupubuz  45718  climinf3  45721  limsupmnflem  45725  limsupmnfuzlem  45731  limsupre3uzlem  45740  climisp  45751  climrescn  45753  climxrrelem  45754  climxrre  45755  xlimmnfv  45839  xlimpnfv  45843  climxlim2lem  45850  cncfioobd  45902  stoweidlem16  46021  stoweidlem28  46033  stoweidlem29  46034  stoweidlem31  46036  stoweidlem35  46040  stoweidlem48  46053  stoweidlem51  46056  stoweidlem52  46057  stoweidlem53  46058  stoweidlem54  46059  stoweidlem56  46061  stoweidlem57  46062  stoweidlem59  46064  stoweidlem60  46065  stoweidlem62  46067  wallispilem3  46072  stirlinglem13  46091  fourierdlem31  46143  fourierdlem39  46151  fourierdlem68  46179  fourierdlem71  46182  fourierdlem73  46184  fourierdlem77  46188  fourierdlem83  46194  fourierdlem87  46198  fourierdlem94  46205  fourierdlem103  46214  fourierdlem104  46215  fourierdlem112  46223  fourierdlem113  46224  salexct  46339  subsaliuncl  46363  sge0lefi  46403  sge0isum  46432  sge0reuzb  46453  iundjiun  46465  voliunsge0lem  46477  meaiuninc3v  46489  ovnsubaddlem2  46576  hoiqssbllem3  46629  vonioo  46687  vonicc  46690  preimageiingt  46725  preimaleiinlt  46726  issmfle  46750  issmfgt  46761  issmfge  46775  smflimlem2  46777  smfsupmpt  46820  smfinflem  46822  smfinfmpt  46824  smfliminflem  46835  fsupdm  46847  finfdm  46851  ffnafv  47176  iccelpart  47438  sprsymrelfo  47502  mogoldbb  47790  sbgoldbo  47792  iunord  49669  setrec1lem2  49681  pgind  49710  aacllem  49794