MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfra1 Structured version   Visualization version   GIF version

Theorem nfra1 2970
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
StepHypRef Expression
1 df-ral 2946 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 2068 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1819 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1521  wnf 1748  wcel 2030  wral 2941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-10 2059
This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1745  df-nf 1750  df-ral 2946
This theorem is referenced by:  hbra1  2971  nfra2  2975  r19.12  3092  ralbi  3097  ralcom2  3133  nfss  3629  rspn0  3967  ralidm  4108  nfii1  4583  dfiun2g  4584  mpteq12f  4764  reusv1  4896  reusv1OLD  4897  reusv2lem1  4898  reusv2lem2  4899  reusv2lem2OLD  4900  reusv2lem3  4901  ralxfrALT  4917  fvmptss  6331  ffnfv  6428  riota5f  6676  mpt2eq123  6756  tfinds  7101  peano5  7131  fun11iun  7168  zfrep6  7176  wfrlem4  7463  tfr3  7540  tz7.48-1  7583  tz7.49  7585  nfixp1  7970  nneneq  8184  scottex  8786  dfac2  8991  infpssrlem4  9166  hsmexlem2  9287  hsmexlem4  9289  domtriomlem  9302  axdc3lem2  9311  axdc3lem4  9313  axdc4lem  9315  zorn2lem5  9360  konigthlem  9428  eltsk2g  9611  dedekind  10238  dedekindle  10239  lble  11013  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  fsuppmapnn0fiubex  12832  prodeq2ii  14687  fprodle  14771  lcmfunsnlem1  15397  lcmfunsnlem2lem1  15398  lcmfunsnlem2  15400  mreiincl  16303  mreexexd  16355  mreexexdOLD  16356  catpropd  16416  acsmapd  17225  gsummatr01lem4  20512  cpmatmcllem  20571  pmatcollpwfi  20635  alexsubALTlem3  21900  isucn2  22130  mptelee  25820  chirred  29382  foresf1o  29469  abrexss  29476  aciunf1lem  29590  nn0min  29695  fprodex01  29699  isarchiofld  29945  reff  30034  locfinreflem  30035  cmpcref  30045  esumcl  30220  measvunilem  30403  measvunilem0  30404  measvuni  30405  voliune  30420  volfiniune  30421  omssubadd  30490  bnj1366  31026  bnj1379  31027  bnj571  31102  bnj1039  31165  bnj1128  31184  bnj1204  31206  bnj1279  31212  bnj1307  31217  bnj1388  31227  bnj1398  31228  bnj1444  31237  bnj1489  31250  bnj1525  31263  dfon2lem3  31814  trpredmintr  31855  frrlem4  31908  nosupbnd1  31985  heicant  33574  cover2  33638  upixp  33654  indexdom  33659  filbcmb  33665  riotasvd  34560  riotasv2d  34561  riotasv2s  34562  glbconxN  34982  pmapglbx  35373  pmapglb2xN  35376  cdleme26ee  35965  cdlemefr29exN  36007  cdlemefs32sn1aw  36019  cdleme43fsv1snlem  36025  cdleme41sn3a  36038  cdleme32d  36049  cdleme32f  36051  cdleme40m  36072  cdleme40n  36073  cdlemk36  36518  cdlemk38  36520  cdlemkid  36541  cdlemk19x  36548  cdlemk11t  36551  mzpexpmpt  37625  gneispace  38749  ssralv2  39054  tratrb  39063  fnchoice  39502  rfcnnnub  39509  uzwo4  39535  ralimralim  39567  ralimda  39640  suprnmpt  39669  fompt  39693  choicefi  39706  axccdom  39730  axccd  39743  rnmptlb  39767  rnmptbddlem  39769  rnmptbd2lem  39777  rnmptbdlem  39784  upbdrech  39833  ssfiunibd  39837  iuneqfzuzlem  39863  infxrunb2  39897  xrralrecnnle  39915  supxrunb3  39936  supxrleubrnmpt  39945  unb2ltle  39955  rexabslelem  39958  allbutfiinf  39960  suprleubrnmpt  39962  uzub  39971  infxrgelbrnmpt  39996  mccl  40148  climsuse  40158  mullimc  40166  islptre  40169  mullimcf  40173  limcrecl  40179  islpcn  40189  limsupre  40191  limcleqr  40194  addlimc  40198  0ellimcdiv  40199  limclner  40201  climinf2lem  40256  limsupubuz  40263  climinf3  40266  limsupmnflem  40270  limsupmnfuzlem  40276  limsupre3uzlem  40285  climisp  40296  climrescn  40298  climxrrelem  40299  climxrre  40300  xlimmnfv  40378  xlimpnfv  40382  climxlim2lem  40389  cncfioobd  40428  stoweidlem16  40551  stoweidlem28  40563  stoweidlem29  40564  stoweidlem31  40566  stoweidlem35  40570  stoweidlem48  40583  stoweidlem51  40586  stoweidlem52  40587  stoweidlem53  40588  stoweidlem54  40589  stoweidlem56  40591  stoweidlem57  40592  stoweidlem59  40594  stoweidlem60  40595  stoweidlem62  40597  wallispilem3  40602  stirlinglem13  40621  fourierdlem31  40673  fourierdlem39  40681  fourierdlem68  40709  fourierdlem71  40712  fourierdlem73  40714  fourierdlem77  40718  fourierdlem83  40724  fourierdlem87  40728  fourierdlem94  40735  fourierdlem103  40744  fourierdlem104  40745  fourierdlem112  40753  fourierdlem113  40754  salexct  40870  subsaliuncl  40894  sge0lefi  40933  sge0isum  40962  sge0reuzb  40983  iundjiun  40995  voliunsge0lem  41007  meaiuninc3v  41019  ovnsubaddlem2  41106  hoiqssbllem3  41159  vonioo  41217  vonicc  41220  preimageiingt  41251  preimaleiinlt  41252  issmfle  41275  issmfgt  41286  issmfge  41299  smflimlem2  41301  smfsupmpt  41342  smfinflem  41344  smfinfmpt  41346  smfliminflem  41357  2reu1  41507  2reu4a  41510  ffnafv  41572  iccelpart  41694  mogoldbb  41998  sbgoldbo  42000  sprsymrelfo  42072  iunord  42747  setrec1lem2  42760  aacllem  42875
  Copyright terms: Public domain W3C validator