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

Theorem nfra1 2606
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 2561 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1768 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1560 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530   F/wnf 1534    e. wcel 1696   A.wral 2556
This theorem is referenced by:  nfra2  2610  r19.12  2669  ralbi  2692  ralcom2  2717  nfss  3186  ralidm  3570  nfii1  3950  dfiun2g  3951  mpteq12f  4112  reusv1  4550  reusv2lem1  4551  reusv2lem2  4552  reusv2lem3  4553  reusv6OLD  4561  ralxfrALT  4569  tfinds  4666  peano5  4695  fun11iun  5509  fvmptss  5625  ffnfv  5701  zfrep6  5764  mpt2eq123  5923  riota5f  6345  riotasvd  6363  riotasvdOLD  6364  riotasv2d  6365  riotasv2dOLD  6366  riotasv2s  6367  riotasv3dOLD  6370  tfrlem1  6407  tfr3  6431  tz7.48-1  6471  tz7.49  6473  nfixp1  6852  nneneq  7060  scottex  7571  dfac2  7773  infpssrlem4  7948  hsmexlem2  8069  hsmexlem4  8071  domtriomlem  8084  axdc3lem2  8093  axdc3lem4  8095  axdc4lem  8097  zorn2lem5  8143  konigthlem  8206  eltsk2g  8389  lble  9722  sumeq2ii  12182  mreiincl  13514  mreexexd  13566  catpropd  13628  acsmapd  14297  alexsubALTlem3  17759  chirred  22991  abrexss  23056  esumcl  23428  esumlef  23450  measvunilem  23555  measvunilem0  23556  measvuni  23557  dedekind  24097  dedekindle  24098  cprodeq2ii  24135  dfon2lem3  24212  trpredmintr  24305  wfrlem4  24330  frrlem4  24355  mptelee  24595  imgfldref2  25167  bwt2  25695  ismonc  25917  cmpmon  25918  isepic  25927  cover2  26461  upixp  26506  indexdom  26516  filbcmb  26535  mzpexpmpt  26926  fnchoice  27803  rfcnnnub  27810  infrglb  27825  climsuse  27837  stoweidlem16  27868  stoweidlem28  27880  stoweidlem29  27881  stoweidlem31  27883  stoweidlem35  27887  stoweidlem48  27900  stoweidlem51  27903  stoweidlem52  27904  stoweidlem53  27905  stoweidlem54  27906  stoweidlem56  27908  stoweidlem57  27909  stoweidlem59  27911  stoweidlem60  27912  stoweidlem62  27914  wallispilem3  27919  stirlinglem13  27938  2reu1  28067  2reu4a  28070  ffnafv  28139  ssralv2  28593  tratrb  28598  bnj1366  29178  bnj1379  29179  bnj571  29254  bnj1039  29317  bnj1128  29336  bnj1204  29358  bnj1279  29364  bnj1309  29368  bnj1307  29369  bnj1388  29379  bnj1398  29380  bnj1444  29389  bnj1489  29402  bnj1525  29415  glbconxN  30189  pmapglbx  30580  pmapglb2xN  30583  cdleme26ee  31171  cdlemefr29exN  31213  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme41sn3a  31244  cdleme32d  31255  cdleme32f  31257  cdleme40m  31278  cdleme40n  31279  cdlemk36  31724  cdlemk38  31726  cdlemkid  31747  cdlemk19x  31754  cdlemk11t  31757
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator