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

Theorem nfra1 2924
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 2900 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 2014 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1770 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1472  wnf 1698  wcel 1976  wral 2895
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-10 2005
This theorem depends on definitions:  df-bi 195  df-or 383  df-ex 1695  df-nf 1700  df-ral 2900
This theorem is referenced by:  hbra1  2925  nfra2  2929  r19.12  3044  ralbi  3049  ralcom2  3082  nfss  3560  rspn0  3891  ralidm  4026  nfii1  4481  dfiun2g  4482  mpteq12f  4655  reusv1  4787  reusv1OLD  4788  reusv2lem1  4789  reusv2lem2  4790  reusv2lem2OLD  4791  reusv2lem3  4792  ralxfrALT  4808  fvmptss  6186  ffnfv  6280  riota5f  6513  mpt2eq123  6590  tfinds  6928  peano5  6958  fun11iun  6996  zfrep6  7004  wfrlem4  7282  tfr3  7359  tz7.48-1  7402  tz7.49  7404  nfixp1  7791  nneneq  8005  scottex  8608  dfac2  8813  infpssrlem4  8988  hsmexlem2  9109  hsmexlem4  9111  domtriomlem  9124  axdc3lem2  9133  axdc3lem4  9135  axdc4lem  9137  zorn2lem5  9182  konigthlem  9246  eltsk2g  9429  dedekind  10051  dedekindle  10052  lble  10824  fsuppmapnn0fiublem  12606  fsuppmapnn0fiub  12607  fsuppmapnn0fiubOLD  12608  fsuppmapnn0fiubex  12609  prodeq2ii  14428  fprodle  14512  lcmfunsnlem1  15134  lcmfunsnlem2lem1  15135  lcmfunsnlem2  15137  mreiincl  16025  mreexexd  16077  mreexexdOLD  16078  catpropd  16138  acsmapd  16947  gsummatr01lem4  20225  cpmatmcllem  20284  pmatcollpwfi  20348  alexsubALTlem3  21605  isucn2  21835  mptelee  25493  chirred  28444  foresf1o  28533  abrexss  28540  aciunf1lem  28650  nn0min  28760  isarchiofld  28954  reff  29040  locfinreflem  29041  cmpcref  29051  esumcl  29225  measvunilem  29408  measvunilem0  29409  measvuni  29410  voliune  29425  volfiniune  29426  omssubadd  29495  bnj1366  29960  bnj1379  29961  bnj571  30036  bnj1039  30099  bnj1128  30118  bnj1204  30140  bnj1279  30146  bnj1307  30151  bnj1388  30161  bnj1398  30162  bnj1444  30171  bnj1489  30184  bnj1525  30197  dfon2lem3  30740  trpredmintr  30781  frrlem4  30833  heicant  32410  cover2  32474  upixp  32490  indexdom  32495  filbcmb  32501  riotasvd  33056  riotasv2d  33057  riotasv2s  33058  glbconxN  33478  pmapglbx  33869  pmapglb2xN  33872  cdleme26ee  34462  cdlemefr29exN  34504  cdlemefs32sn1aw  34516  cdleme43fsv1snlem  34522  cdleme41sn3a  34535  cdleme32d  34546  cdleme32f  34548  cdleme40m  34569  cdleme40n  34570  cdlemk36  35015  cdlemk38  35017  cdlemkid  35038  cdlemk19x  35045  cdlemk11t  35048  mzpexpmpt  36122  gneispace  37248  ssralv2  37554  tratrb  37563  fnchoice  38007  rfcnnnub  38014  uzwo4  38042  ralimralim  38075  suprnmpt  38146  fompt  38170  choicefi  38183  axccdom  38207  axccd  38220  upbdrech  38256  ssfiunibd  38260  iuneqfzuzlem  38288  infxrunb2  38322  xrralrecnnle  38340  mccl  38462  climsuse  38472  mullimc  38480  islptre  38483  mullimcf  38487  limcrecl  38493  islpcn  38503  limsupre  38505  limcleqr  38508  addlimc  38512  0ellimcdiv  38513  limclner  38515  cncfioobd  38580  stoweidlem16  38706  stoweidlem28  38718  stoweidlem29  38719  stoweidlem31  38721  stoweidlem35  38725  stoweidlem48  38738  stoweidlem51  38741  stoweidlem52  38742  stoweidlem53  38743  stoweidlem54  38744  stoweidlem56  38746  stoweidlem57  38747  stoweidlem59  38749  stoweidlem60  38750  stoweidlem62  38752  wallispilem3  38757  stirlinglem13  38776  fourierdlem31  38828  fourierdlem39  38836  fourierdlem68  38864  fourierdlem71  38867  fourierdlem73  38869  fourierdlem77  38873  fourierdlem83  38879  fourierdlem87  38883  fourierdlem94  38890  fourierdlem103  38899  fourierdlem104  38900  fourierdlem112  38908  fourierdlem113  38909  salexct  39025  subsaliuncl  39049  sge0lefi  39088  sge0isum  39117  sge0reuzb  39138  iundjiun  39150  voliunsge0lem  39162  ovnsubaddlem2  39258  hoiqssbllem3  39311  vonioo  39370  vonicc  39373  preimageiingt  39404  preimaleiinlt  39405  issmfle  39429  issmfgt  39440  issmfge  39453  smflimlem2  39455  2reu1  39632  2reu4a  39635  ffnafv  39698  iccelpart  39769  aacllem  42312
  Copyright terms: Public domain W3C validator