Theorem nfra1 3261

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

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

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 3045

This theorem is referenced by:  hbra1  3275  r19.12  3288  nfra2  3350  ralcom2  3351  2reu1  3860  nfss  3939  2reu4lem  4485  iuneqconst  4967  nfii1  4993  dfiun2gOLD  4995  mpteq12f  5192  reusv1  5352  reusv2lem1  5353  reusv2lem2  5354  reusv2lem3  5355  ralxfrALT  5370  fvmptss  6980  fompt  7090  ffnfv  7091  riota5f  7372  mpoeq123  7461  tfinds  7836  zfrep6  7933  frrlem4  8268  tfr3  8367  tz7.48-1  8411  tz7.49  8413  naddsuc2  8665  nfixp1  8891  nneneq  9170  scottex  9838  dfac2b  10084  infpssrlem4  10259  hsmexlem2  10380  hsmexlem4  10382  domtriomlem  10395  axdc3lem2  10404  axdc3lem4  10406  axdc4lem  10408  zorn2lem5  10453  konigthlem  10521  eltsk2g  10704  dedekind  11337  dedekindle  11338  lble  12135  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  fsuppmapnn0fiubex  13957  prodeq2ii  15877  fprodle  15962  lcmfunsnlem1  16607  lcmfunsnlem2lem1  16608  lcmfunsnlem2  16610  mreiincl  17557  mreexexd  17609  catpropd  17670  acsmapd  18513  gsummatr01lem4  22545  cpmatmcllem  22605  alexsubALTlem3  23936  isucn2  24166  nosupbnd1  27626  noinfbnd1  27641  mptelee  28822  chirred  32324  opreu2reuALT  32406  foresf1o  32433  abrexss  32441  iinabrex  32498  aciunf1lem  32586  nn0min  32745  fprodex01  32750  isarchiofld  33295  elrspunidl  33399  reff  33829  locfinreflem  33830  cmpcref  33840  zarcmplem  33871  esumcl  34020  measvunilem  34202  measvunilem0  34203  measvuni  34204  voliune  34219  volfiniune  34220  omssubadd  34291  bnj1366  34819  bnj1379  34820  bnj571  34896  bnj1039  34961  bnj1128  34980  bnj1204  35002  bnj1279  35008  bnj1307  35013  bnj1388  35023  bnj1398  35024  bnj1444  35033  bnj1489  35046  bnj1525  35059  dfon2lem3  35773  domalom  37392  ralssiun  37395  fvineqsneu  37399  fvineqsneq  37400  heicant  37649  cover2  37709  upixp  37723  indexdom  37728  filbcmb  37734  riotasvd  38949  riotasv2d  38950  riotasv2s  38951  glbconxN  39372  pmapglbx  39763  pmapglb2xN  39766  cdleme26ee  40354  cdlemefr29exN  40396  cdlemefs32sn1aw  40408  cdleme43fsv1snlem  40414  cdleme41sn3a  40427  cdleme32d  40438  cdleme32f  40440  cdleme40m  40461  cdleme40n  40462  cdlemk36  40907  cdlemk38  40909  cdlemkid  40930  cdlemk19x  40937  cdlemk11t  40940  mzpexpmpt  42733  nadd1suc  43381  gneispace  44123  mnuprdlem4  44264  ssralv2  44521  tratrb  44526  modelaxrep  44971  fnchoice  45023  rfcnnnub  45030  uzwo4  45047  ralimralim  45075  suprnmpt  45168  choicefi  45194  axccdom  45216  axccd  45223  rnmptlb  45237  rnmptbddlem  45238  rnmptbd2lem  45242  rnmptbdlem  45249  upbdrech  45303  ssfiunibd  45307  iuneqfzuzlem  45330  infxrunb2  45364  xrralrecnnle  45379  supxrunb3  45395  supxrleubrnmpt  45402  unb2ltle  45411  rexabslelem  45414  allbutfiinf  45416  suprleubrnmpt  45418  uzub  45427  infxrgelbrnmpt  45450  cvgcaule  45487  mccl  45596  climsuse  45606  mullimc  45614  islptre  45617  mullimcf  45621  limcrecl  45627  islpcn  45637  limsupre  45639  limcleqr  45642  addlimc  45646  0ellimcdiv  45647  limclner  45649  climinf2lem  45704  limsupubuz  45711  climinf3  45714  limsupmnflem  45718  limsupmnfuzlem  45724  limsupre3uzlem  45733  climisp  45744  climrescn  45746  climxrrelem  45747  climxrre  45748  xlimmnfv  45832  xlimpnfv  45836  climxlim2lem  45843  cncfioobd  45895  stoweidlem16  46014  stoweidlem28  46026  stoweidlem29  46027  stoweidlem31  46029  stoweidlem35  46033  stoweidlem48  46046  stoweidlem51  46049  stoweidlem52  46050  stoweidlem53  46051  stoweidlem54  46052  stoweidlem56  46054  stoweidlem57  46055  stoweidlem59  46057  stoweidlem60  46058  stoweidlem62  46060  wallispilem3  46065  stirlinglem13  46084  fourierdlem31  46136  fourierdlem39  46144  fourierdlem68  46172  fourierdlem71  46175  fourierdlem73  46177  fourierdlem77  46181  fourierdlem83  46187  fourierdlem87  46191  fourierdlem94  46198  fourierdlem103  46207  fourierdlem104  46208  fourierdlem112  46216  fourierdlem113  46217  salexct  46332  subsaliuncl  46356  sge0lefi  46396  sge0isum  46425  sge0reuzb  46446  iundjiun  46458  voliunsge0lem  46470  meaiuninc3v  46482  ovnsubaddlem2  46569  hoiqssbllem3  46622  vonioo  46680  vonicc  46683  preimageiingt  46718  preimaleiinlt  46719  issmfle  46743  issmfgt  46754  issmfge  46768  smflimlem2  46770  smfsupmpt  46813  smfinflem  46815  smfinfmpt  46817  smfliminflem  46828  fsupdm  46840  finfdm  46844  ffnafv  47172  iccelpart  47434  sprsymrelfo  47498  mogoldbb  47786  sbgoldbo  47788  iunord  49665  setrec1lem2  49677  pgind  49706  aacllem  49790