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

Theorem nfra1 2938
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 2914 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 2026 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1777 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1479  wnf 1706  wcel 1988  wral 2909
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-10 2017
This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1703  df-nf 1708  df-ral 2914
This theorem is referenced by:  hbra1  2939  nfra2  2943  r19.12  3059  ralbi  3064  ralcom2  3099  nfss  3588  rspn0  3926  ralidm  4066  nfii1  4542  dfiun2g  4543  mpteq12f  4722  reusv1  4857  reusv1OLD  4858  reusv2lem1  4859  reusv2lem2  4860  reusv2lem2OLD  4861  reusv2lem3  4862  ralxfrALT  4878  fvmptss  6279  ffnfv  6374  riota5f  6621  mpt2eq123  6699  tfinds  7044  peano5  7074  fun11iun  7111  zfrep6  7119  wfrlem4  7403  tfr3  7480  tz7.48-1  7523  tz7.49  7525  nfixp1  7913  nneneq  8128  scottex  8733  dfac2  8938  infpssrlem4  9113  hsmexlem2  9234  hsmexlem4  9236  domtriomlem  9249  axdc3lem2  9258  axdc3lem4  9260  axdc4lem  9262  zorn2lem5  9307  konigthlem  9375  eltsk2g  9558  dedekind  10185  dedekindle  10186  lble  10960  fsuppmapnn0fiublem  12772  fsuppmapnn0fiub  12773  fsuppmapnn0fiubOLD  12774  fsuppmapnn0fiubex  12775  prodeq2ii  14624  fprodle  14708  lcmfunsnlem1  15331  lcmfunsnlem2lem1  15332  lcmfunsnlem2  15334  mreiincl  16237  mreexexd  16289  mreexexdOLD  16290  catpropd  16350  acsmapd  17159  gsummatr01lem4  20445  cpmatmcllem  20504  pmatcollpwfi  20568  alexsubALTlem3  21834  isucn2  22064  mptelee  25756  chirred  29224  foresf1o  29315  abrexss  29322  aciunf1lem  29435  nn0min  29541  fprodex01  29545  isarchiofld  29791  reff  29880  locfinreflem  29881  cmpcref  29891  esumcl  30066  measvunilem  30249  measvunilem0  30250  measvuni  30251  voliune  30266  volfiniune  30267  omssubadd  30336  bnj1366  30874  bnj1379  30875  bnj571  30950  bnj1039  31013  bnj1128  31032  bnj1204  31054  bnj1279  31060  bnj1307  31065  bnj1388  31075  bnj1398  31076  bnj1444  31085  bnj1489  31098  bnj1525  31111  dfon2lem3  31664  trpredmintr  31705  frrlem4  31757  nosupbnd1  31834  heicant  33415  cover2  33479  upixp  33495  indexdom  33500  filbcmb  33506  riotasvd  34061  riotasv2d  34062  riotasv2s  34063  glbconxN  34483  pmapglbx  34874  pmapglb2xN  34877  cdleme26ee  35467  cdlemefr29exN  35509  cdlemefs32sn1aw  35521  cdleme43fsv1snlem  35527  cdleme41sn3a  35540  cdleme32d  35551  cdleme32f  35553  cdleme40m  35574  cdleme40n  35575  cdlemk36  36020  cdlemk38  36022  cdlemkid  36043  cdlemk19x  36050  cdlemk11t  36053  mzpexpmpt  37127  gneispace  38252  ssralv2  38557  tratrb  38566  fnchoice  39008  rfcnnnub  39015  uzwo4  39041  ralimralim  39073  ralimda  39146  suprnmpt  39171  fompt  39195  choicefi  39208  axccdom  39232  axccd  39245  rnmptlb  39269  rnmptbddlem  39271  rnmptbd2lem  39279  rnmptbdlem  39286  upbdrech  39332  ssfiunibd  39336  iuneqfzuzlem  39363  infxrunb2  39397  xrralrecnnle  39415  supxrunb3  39436  supxrleubrnmpt  39445  unb2ltle  39455  rexabslelem  39458  allbutfiinf  39460  suprleubrnmpt  39462  uzub  39471  infxrgelbrnmpt  39496  mccl  39630  climsuse  39640  mullimc  39648  islptre  39651  mullimcf  39655  limcrecl  39661  islpcn  39671  limsupre  39673  limcleqr  39676  addlimc  39680  0ellimcdiv  39681  limclner  39683  climinf2lem  39738  limsupubuz  39745  climinf3  39748  limsupmnflem  39752  limsupmnfuzlem  39758  limsupre3uzlem  39767  cncfioobd  39873  stoweidlem16  39996  stoweidlem28  40008  stoweidlem29  40009  stoweidlem31  40011  stoweidlem35  40015  stoweidlem48  40028  stoweidlem51  40031  stoweidlem52  40032  stoweidlem53  40033  stoweidlem54  40034  stoweidlem56  40036  stoweidlem57  40037  stoweidlem59  40039  stoweidlem60  40040  stoweidlem62  40042  wallispilem3  40047  stirlinglem13  40066  fourierdlem31  40118  fourierdlem39  40126  fourierdlem68  40154  fourierdlem71  40157  fourierdlem73  40159  fourierdlem77  40163  fourierdlem83  40169  fourierdlem87  40173  fourierdlem94  40180  fourierdlem103  40189  fourierdlem104  40190  fourierdlem112  40198  fourierdlem113  40199  salexct  40315  subsaliuncl  40339  sge0lefi  40378  sge0isum  40407  sge0reuzb  40428  iundjiun  40440  voliunsge0lem  40452  ovnsubaddlem2  40548  hoiqssbllem3  40601  vonioo  40659  vonicc  40662  preimageiingt  40693  preimaleiinlt  40694  issmfle  40717  issmfgt  40728  issmfge  40741  smflimlem2  40743  smfsupmpt  40784  smfinflem  40786  smfinfmpt  40788  smfliminflem  40799  2reu1  40949  2reu4a  40952  ffnafv  41014  iccelpart  41133  mogoldbb  41438  sbgoldbo  41440  sprsymrelfo  41512  iunord  42187  setrec1lem2  42200  aacllem  42312
  Copyright terms: Public domain W3C validator