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

Theorem nfra1 2593
Description:  x is not free in  A. x  e.  A ph. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfra1  |-  F/ x A. x  e.  A  ph

Proof of Theorem nfra1
StepHypRef Expression
1 df-ral 2548 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1756 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1557 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527   F/wnf 1531    e. wcel 1684   A.wral 2543
This theorem is referenced by:  nfra2  2597  r19.12  2656  ralbi  2679  ralcom2  2704  nfss  3173  ralidm  3557  nfii1  3934  dfiun2g  3935  mpteq12f  4096  reusv1  4534  reusv2lem1  4535  reusv2lem2  4536  reusv2lem3  4537  reusv6OLD  4545  ralxfrALT  4553  tfinds  4650  peano5  4679  fun11iun  5493  fvmptss  5609  ffnfv  5685  zfrep6  5748  mpt2eq123  5907  riota5f  6329  riotasvd  6347  riotasvdOLD  6348  riotasv2d  6349  riotasv2dOLD  6350  riotasv2s  6351  riotasv3dOLD  6354  tfrlem1  6391  tfr3  6415  tz7.48-1  6455  tz7.49  6457  nfixp1  6836  nneneq  7044  scottex  7555  dfac2  7757  infpssrlem4  7932  hsmexlem2  8053  hsmexlem4  8055  domtriomlem  8068  axdc3lem2  8077  axdc3lem4  8079  axdc4lem  8081  zorn2lem5  8127  konigthlem  8190  eltsk2g  8373  lble  9706  sumeq2ii  12166  mreiincl  13498  mreexexd  13550  catpropd  13612  acsmapd  14281  alexsubALTlem3  17743  chirred  22975  abrexss  23040  esumcl  23413  esumlef  23435  measvunilem  23540  measvunilem0  23541  measvuni  23542  dedekind  24082  dedekindle  24083  dfon2lem3  24141  trpredmintr  24234  wfrlem4  24259  frrlem4  24284  mptelee  24523  imgfldref2  25064  bwt2  25592  ismonc  25814  cmpmon  25815  isepic  25824  cover2  26358  upixp  26403  indexdom  26413  filbcmb  26432  mzpexpmpt  26823  fnchoice  27700  rfcnnnub  27707  infrglb  27722  climsuse  27734  stoweidlem16  27765  stoweidlem28  27777  stoweidlem29  27778  stoweidlem31  27780  stoweidlem35  27784  stoweidlem48  27797  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem56  27805  stoweidlem57  27806  stoweidlem59  27808  stoweidlem60  27809  stoweidlem62  27811  wallispilem3  27816  stirlinglem13  27835  2reu1  27964  2reu4a  27967  ffnafv  28033  ssralv2  28294  tratrb  28299  bnj1366  28862  bnj1379  28863  bnj571  28938  bnj1039  29001  bnj1128  29020  bnj1204  29042  bnj1279  29048  bnj1309  29052  bnj1307  29053  bnj1388  29063  bnj1398  29064  bnj1444  29073  bnj1489  29086  bnj1525  29099  glbconxN  29567  pmapglbx  29958  pmapglb2xN  29961  cdleme26ee  30549  cdlemefr29exN  30591  cdlemefs32sn1aw  30603  cdleme43fsv1snlem  30609  cdleme41sn3a  30622  cdleme32d  30633  cdleme32f  30635  cdleme40m  30656  cdleme40n  30657  cdlemk36  31102  cdlemk38  31104  cdlemkid  31125  cdlemk19x  31132  cdlemk11t  31135
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator