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

Theorem nfra1 3088
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 3060 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 2193 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1948 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1650  wnf 1878  wcel 2155  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-10 2183
This theorem depends on definitions:  df-bi 198  df-or 874  df-ex 1875  df-nf 1879  df-ral 3060
This theorem is referenced by:  hbra1  3089  nfra2  3093  r19.12  3210  ralbi  3215  ralcom2  3251  nfss  3754  rspn0  4098  ralidm  4234  nfii1  4707  dfiun2g  4708  mpteq12f  4890  reusv1  5032  reusv2lem1  5033  reusv2lem2  5034  reusv2lem3  5035  ralxfrALT  5050  fvmptss  6481  ffnfv  6578  riota5f  6828  mpt2eq123  6912  tfinds  7257  peano5  7287  fun11iun  7324  zfrep6  7332  wfrlem4  7621  wfrlem4OLD  7622  tfr3  7699  tz7.48-1  7742  tz7.49  7744  nfixp1  8133  nneneq  8350  scottex  8963  dfac2b  9204  dfac2OLD  9206  infpssrlem4  9381  hsmexlem2  9502  hsmexlem4  9504  domtriomlem  9517  axdc3lem2  9526  axdc3lem4  9528  axdc4lem  9530  zorn2lem5  9575  konigthlem  9643  eltsk2g  9826  dedekind  10454  dedekindle  10455  lble  11229  fsuppmapnn0fiublem  12997  fsuppmapnn0fiub  12998  fsuppmapnn0fiubex  12999  prodeq2ii  14928  fprodle  15011  lcmfunsnlem1  15633  lcmfunsnlem2lem1  15634  lcmfunsnlem2  15636  mreiincl  16524  mreexexd  16576  catpropd  16636  acsmapd  17446  gsummatr01lem4  20742  cpmatmcllem  20802  alexsubALTlem3  22132  isucn2  22362  mptelee  26066  chirred  29645  foresf1o  29727  abrexss  29734  aciunf1lem  29847  nn0min  29951  fprodex01  29955  isarchiofld  30199  reff  30288  locfinreflem  30289  cmpcref  30299  esumcl  30474  measvunilem  30657  measvunilem0  30658  measvuni  30659  voliune  30674  volfiniune  30675  omssubadd  30744  bnj1366  31280  bnj1379  31281  bnj571  31356  bnj1039  31419  bnj1128  31438  bnj1204  31460  bnj1279  31466  bnj1307  31471  bnj1388  31481  bnj1398  31482  bnj1444  31491  bnj1489  31504  bnj1525  31517  dfon2lem3  32065  trpredmintr  32106  frrlem4  32159  nosupbnd1  32236  heicant  33800  cover2  33863  upixp  33879  indexdom  33884  filbcmb  33890  riotasvd  34844  riotasv2d  34845  riotasv2s  34846  glbconxN  35266  pmapglbx  35657  pmapglb2xN  35660  cdleme26ee  36248  cdlemefr29exN  36290  cdlemefs32sn1aw  36302  cdleme43fsv1snlem  36308  cdleme41sn3a  36321  cdleme32d  36332  cdleme32f  36334  cdleme40m  36355  cdleme40n  36356  cdlemk36  36801  cdlemk38  36803  cdlemkid  36824  cdlemk19x  36831  cdlemk11t  36834  mzpexpmpt  37918  gneispace  39038  ssralv2  39341  tratrb  39346  fnchoice  39772  rfcnnnub  39779  uzwo4  39804  ralimralim  39836  ralimda  39907  suprnmpt  39934  fompt  39958  choicefi  39969  axccdom  39993  axccd  40003  rnmptlb  40027  rnmptbddlem  40029  rnmptbd2lem  40036  rnmptbdlem  40043  upbdrech  40090  ssfiunibd  40094  iuneqfzuzlem  40120  infxrunb2  40154  xrralrecnnle  40172  supxrunb3  40192  supxrleubrnmpt  40201  unb2ltle  40211  rexabslelem  40214  allbutfiinf  40216  suprleubrnmpt  40218  uzub  40227  infxrgelbrnmpt  40252  mccl  40400  climsuse  40410  mullimc  40418  islptre  40421  mullimcf  40425  limcrecl  40431  islpcn  40441  limsupre  40443  limcleqr  40446  addlimc  40450  0ellimcdiv  40451  limclner  40453  climinf2lem  40508  limsupubuz  40515  climinf3  40518  limsupmnflem  40522  limsupmnfuzlem  40528  limsupre3uzlem  40537  climisp  40548  climrescn  40550  climxrrelem  40551  climxrre  40552  xlimmnfv  40630  xlimpnfv  40634  climxlim2lem  40641  cncfioobd  40680  stoweidlem16  40802  stoweidlem28  40814  stoweidlem29  40815  stoweidlem31  40817  stoweidlem35  40821  stoweidlem48  40834  stoweidlem51  40837  stoweidlem52  40838  stoweidlem53  40839  stoweidlem54  40840  stoweidlem56  40842  stoweidlem57  40843  stoweidlem59  40845  stoweidlem60  40846  stoweidlem62  40848  wallispilem3  40853  stirlinglem13  40872  fourierdlem31  40924  fourierdlem39  40932  fourierdlem68  40960  fourierdlem71  40963  fourierdlem73  40965  fourierdlem77  40969  fourierdlem83  40975  fourierdlem87  40979  fourierdlem94  40986  fourierdlem103  40995  fourierdlem104  40996  fourierdlem112  41004  fourierdlem113  41005  salexct  41121  subsaliuncl  41145  sge0lefi  41184  sge0isum  41213  sge0reuzb  41234  iundjiun  41246  voliunsge0lem  41258  meaiuninc3v  41270  ovnsubaddlem2  41357  hoiqssbllem3  41410  vonioo  41468  vonicc  41471  preimageiingt  41502  preimaleiinlt  41503  issmfle  41526  issmfgt  41537  issmfge  41550  smflimlem2  41552  smfsupmpt  41593  smfinflem  41595  smfinfmpt  41597  smfliminflem  41608  2reu1  41789  2reu4a  41792  ffnafv  41851  iccelpart  42035  mogoldbb  42281  sbgoldbo  42283  sprsymrelfo  42348  iunord  43023  setrec1lem2  43036  aacllem  43151
  Copyright terms: Public domain W3C validator