Theorem nfra1 3219

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

Syntax hints:   → wi 4  ∀wal 1531  Ⅎwnf 1780   ∈ wcel 2110  ∀wral 3138

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

This theorem depends on definitions:  df-bi 209  df-or 844  df-ex 1777  df-nf 1781  df-ral 3143

This theorem is referenced by:  hbra1  3220  nfra2w  3227  nfra2  3228  ralbiOLD  3233  ralrexbidOLD  3323  r19.12  3324  r19.12OLD  3327  ralcom2  3363  2reu1  3880  nfss  3959  rspn0  4312  ralidm  4454  2reu4lem  4464  iuneqconst  4922  nfii1  4946  dfiun2g  4947  dfiun2gOLD  4948  mpteq12f  5141  reusv1  5289  reusv2lem1  5290  reusv2lem2  5291  reusv2lem3  5292  ralxfrALT  5307  fvmptss  6774  ffnfv  6876  riota5f  7136  mpoeq123  7220  tfinds  7568  peano5  7599  zfrep6  7650  wfrlem4  7952  tfr3  8029  tz7.48-1  8073  tz7.49  8075  nfixp1  8476  nneneq  8694  scottex  9308  dfac2b  9550  infpssrlem4  9722  hsmexlem2  9843  hsmexlem4  9845  domtriomlem  9858  axdc3lem2  9867  axdc3lem4  9869  axdc4lem  9871  zorn2lem5  9916  konigthlem  9984  eltsk2g  10167  dedekind  10797  dedekindle  10798  lble  11587  fsuppmapnn0fiublem  13352  fsuppmapnn0fiub  13353  fsuppmapnn0fiubex  13354  prodeq2ii  15261  fprodle  15344  lcmfunsnlem1  15975  lcmfunsnlem2lem1  15976  lcmfunsnlem2  15978  mreiincl  16861  mreexexd  16913  catpropd  16973  acsmapd  17782  gsummatr01lem4  21261  cpmatmcllem  21320  alexsubALTlem3  22651  isucn2  22882  mptelee  26675  chirred  30166  opreu2reuALT  30234  foresf1o  30259  abrexss  30266  aciunf1lem  30401  nn0min  30531  fprodex01  30536  isarchiofld  30885  reff  31098  locfinreflem  31099  cmpcref  31109  esumcl  31284  measvunilem  31466  measvunilem0  31467  measvuni  31468  voliune  31483  volfiniune  31484  omssubadd  31553  bnj1366  32096  bnj1379  32097  bnj571  32173  bnj1039  32238  bnj1128  32257  bnj1204  32279  bnj1279  32285  bnj1307  32290  bnj1388  32300  bnj1398  32301  bnj1444  32310  bnj1489  32323  bnj1525  32336  dfon2lem3  33025  trpredmintr  33065  frrlem4  33121  nosupbnd1  33209  domalom  34679  ralssiun  34682  fvineqsneu  34686  fvineqsneq  34687  heicant  34921  cover2  34983  upixp  34998  indexdom  35003  filbcmb  35009  riotasvd  36086  riotasv2d  36087  riotasv2s  36088  glbconxN  36508  pmapglbx  36899  pmapglb2xN  36902  cdleme26ee  37490  cdlemefr29exN  37532  cdlemefs32sn1aw  37544  cdleme43fsv1snlem  37550  cdleme41sn3a  37563  cdleme32d  37574  cdleme32f  37576  cdleme40m  37597  cdleme40n  37598  cdlemk36  38043  cdlemk38  38045  cdlemkid  38066  cdlemk19x  38073  cdlemk11t  38076  mzpexpmpt  39335  gneispace  40477  mnuprdlem4  40604  ssralv2  40858  tratrb  40863  fnchoice  41279  rfcnnnub  41286  uzwo4  41308  ralimralim  41338  ralimda  41399  suprnmpt  41423  fompt  41446  choicefi  41456  axccdom  41480  axccd  41488  rnmptlb  41507  rnmptbddlem  41508  rnmptbd2lem  41513  rnmptbdlem  41520  upbdrech  41565  ssfiunibd  41569  iuneqfzuzlem  41595  infxrunb2  41629  xrralrecnnle  41646  supxrunb3  41665  supxrleubrnmpt  41672  unb2ltle  41682  rexabslelem  41685  allbutfiinf  41687  suprleubrnmpt  41689  uzub  41698  infxrgelbrnmpt  41723  mccl  41872  climsuse  41882  mullimc  41890  islptre  41893  mullimcf  41897  limcrecl  41903  islpcn  41913  limsupre  41915  limcleqr  41918  addlimc  41922  0ellimcdiv  41923  limclner  41925  climinf2lem  41980  limsupubuz  41987  climinf3  41990  limsupmnflem  41994  limsupmnfuzlem  42000  limsupre3uzlem  42009  climisp  42020  climrescn  42022  climxrrelem  42023  climxrre  42024  xlimmnfv  42108  xlimpnfv  42112  climxlim2lem  42119  cncfioobd  42173  stoweidlem16  42295  stoweidlem28  42307  stoweidlem29  42308  stoweidlem31  42310  stoweidlem35  42314  stoweidlem48  42327  stoweidlem51  42330  stoweidlem52  42331  stoweidlem53  42332  stoweidlem54  42333  stoweidlem56  42335  stoweidlem57  42336  stoweidlem59  42338  stoweidlem60  42339  stoweidlem62  42341  wallispilem3  42346  stirlinglem13  42365  fourierdlem31  42417  fourierdlem39  42425  fourierdlem68  42453  fourierdlem71  42456  fourierdlem73  42458  fourierdlem77  42462  fourierdlem83  42468  fourierdlem87  42472  fourierdlem94  42479  fourierdlem103  42488  fourierdlem104  42489  fourierdlem112  42497  fourierdlem113  42498  salexct  42611  subsaliuncl  42635  sge0lefi  42674  sge0isum  42703  sge0reuzb  42724  iundjiun  42736  voliunsge0lem  42748  meaiuninc3v  42760  ovnsubaddlem2  42847  hoiqssbllem3  42900  vonioo  42958  vonicc  42961  preimageiingt  42992  preimaleiinlt  42993  issmfle  43016  issmfgt  43027  issmfge  43040  smflimlem2  43042  smfsupmpt  43083  smfinflem  43085  smfinfmpt  43087  smfliminflem  43098  ffnafv  43364  iccelpart  43587  sprsymrelfo  43653  mogoldbb  43944  sbgoldbo  43946  iunord  44773  setrec1lem2  44785  aacllem  44896