Theorem nfra1 3280

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

Syntax hints:   → wi 4  ∀wal 1538  Ⅎwnf 1784   ∈ wcel 2105  ∀wral 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2136

This theorem depends on definitions:  df-bi 206  df-or 845  df-ex 1781  df-nf 1785  df-ral 3061

This theorem is referenced by:  hbra1  3297  r19.12  3310  r19.12OLD  3311  nfra2wOLDOLD  3318  nfra2  3371  ralcom2  3372  2reu1  3891  nfss  3974  rspn0OLD  4353  ralidmOLD  4515  2reu4lem  4525  iuneqconst  5008  nfii1  5032  dfiun2gOLD  5034  mpteq12f  5236  reusv1  5395  reusv2lem1  5396  reusv2lem2  5397  reusv2lem3  5398  ralxfrALT  5413  fvmptss  7010  fompt  7119  ffnfv  7120  riota5f  7397  mpoeq123  7484  tfinds  7853  peano5OLD  7889  zfrep6  7945  frrlem4  8280  wfrlem4OLD  8318  tfr3  8405  tz7.48-1  8449  tz7.49  8451  nfixp1  8918  nneneq  9215  nneneqOLD  9227  scottex  9886  dfac2b  10131  infpssrlem4  10307  hsmexlem2  10428  hsmexlem4  10430  domtriomlem  10443  axdc3lem2  10452  axdc3lem4  10454  axdc4lem  10456  zorn2lem5  10501  konigthlem  10569  eltsk2g  10752  dedekind  11384  dedekindle  11385  lble  12173  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  fsuppmapnn0fiubex  13964  prodeq2ii  15864  fprodle  15947  lcmfunsnlem1  16581  lcmfunsnlem2lem1  16582  lcmfunsnlem2  16584  mreiincl  17547  mreexexd  17599  catpropd  17660  acsmapd  18517  gsummatr01lem4  22480  cpmatmcllem  22540  alexsubALTlem3  23873  isucn2  24104  nosupbnd1  27561  noinfbnd1  27576  mptelee  28587  chirred  32082  opreu2reuALT  32151  foresf1o  32176  abrexss  32183  iinabrex  32234  aciunf1lem  32321  nn0min  32460  fprodex01  32465  isarchiofld  32872  elrspunidl  32987  reff  33284  locfinreflem  33285  cmpcref  33295  zarcmplem  33326  esumcl  33493  measvunilem  33675  measvunilem0  33676  measvuni  33677  voliune  33692  volfiniune  33693  omssubadd  33764  bnj1366  34305  bnj1379  34306  bnj571  34382  bnj1039  34447  bnj1128  34466  bnj1204  34488  bnj1279  34494  bnj1307  34499  bnj1388  34509  bnj1398  34510  bnj1444  34519  bnj1489  34532  bnj1525  34545  dfon2lem3  35228  domalom  36751  ralssiun  36754  fvineqsneu  36758  fvineqsneq  36759  heicant  36989  cover2  37049  upixp  37063  indexdom  37068  filbcmb  37074  riotasvd  38292  riotasv2d  38293  riotasv2s  38294  glbconxN  38715  pmapglbx  39106  pmapglb2xN  39109  cdleme26ee  39697  cdlemefr29exN  39739  cdlemefs32sn1aw  39751  cdleme43fsv1snlem  39757  cdleme41sn3a  39770  cdleme32d  39781  cdleme32f  39783  cdleme40m  39804  cdleme40n  39805  cdlemk36  40250  cdlemk38  40252  cdlemkid  40273  cdlemk19x  40280  cdlemk11t  40283  mzpexpmpt  41948  nadd1suc  42607  naddsuc2  42608  gneispace  43350  mnuprdlem4  43499  ssralv2  43757  tratrb  43762  fnchoice  44178  rfcnnnub  44185  uzwo4  44204  ralimralim  44234  suprnmpt  44334  choicefi  44360  axccdom  44382  axccd  44389  rnmptlb  44408  rnmptbddlem  44409  rnmptbd2lem  44413  rnmptbdlem  44420  upbdrech  44476  ssfiunibd  44480  iuneqfzuzlem  44505  infxrunb2  44539  xrralrecnnle  44554  supxrunb3  44570  supxrleubrnmpt  44577  unb2ltle  44586  rexabslelem  44589  allbutfiinf  44591  suprleubrnmpt  44593  uzub  44602  infxrgelbrnmpt  44625  cvgcaule  44663  mccl  44775  climsuse  44785  mullimc  44793  islptre  44796  mullimcf  44800  limcrecl  44806  islpcn  44816  limsupre  44818  limcleqr  44821  addlimc  44825  0ellimcdiv  44826  limclner  44828  climinf2lem  44883  limsupubuz  44890  climinf3  44893  limsupmnflem  44897  limsupmnfuzlem  44903  limsupre3uzlem  44912  climisp  44923  climrescn  44925  climxrrelem  44926  climxrre  44927  xlimmnfv  45011  xlimpnfv  45015  climxlim2lem  45022  cncfioobd  45074  stoweidlem16  45193  stoweidlem28  45205  stoweidlem29  45206  stoweidlem31  45208  stoweidlem35  45212  stoweidlem48  45225  stoweidlem51  45228  stoweidlem52  45229  stoweidlem53  45230  stoweidlem54  45231  stoweidlem56  45233  stoweidlem57  45234  stoweidlem59  45236  stoweidlem60  45237  stoweidlem62  45239  wallispilem3  45244  stirlinglem13  45263  fourierdlem31  45315  fourierdlem39  45323  fourierdlem68  45351  fourierdlem71  45354  fourierdlem73  45356  fourierdlem77  45360  fourierdlem83  45366  fourierdlem87  45370  fourierdlem94  45377  fourierdlem103  45386  fourierdlem104  45387  fourierdlem112  45395  fourierdlem113  45396  salexct  45511  subsaliuncl  45535  sge0lefi  45575  sge0isum  45604  sge0reuzb  45625  iundjiun  45637  voliunsge0lem  45649  meaiuninc3v  45661  ovnsubaddlem2  45748  hoiqssbllem3  45801  vonioo  45859  vonicc  45862  preimageiingt  45897  preimaleiinlt  45898  issmfle  45922  issmfgt  45933  issmfge  45947  smflimlem2  45949  smfsupmpt  45992  smfinflem  45994  smfinfmpt  45996  smfliminflem  46007  fsupdm  46019  finfdm  46023  ffnafv  46340  iccelpart  46562  sprsymrelfo  46626  mogoldbb  46914  sbgoldbo  46916  iunord  47885  setrec1lem2  47897  pgind  47926  aacllem  48012