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

Theorem nfre1 2599
Description:  x is not free in  E. x  e.  A ph. (Contributed by NM, 19-Mar-1997.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfre1  |-  F/ x E. x  e.  A  ph

Proof of Theorem nfre1
StepHypRef Expression
1 df-rex 2549 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 nfe1 1706 . 2  |-  F/ x E. x ( x  e.  A  /\  ph )
31, 2nfxfr 1557 1  |-  F/ x E. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1528   F/wnf 1531    e. wcel 1684   E.wrex 2544
This theorem is referenced by:  2rmorex  2969  nfiu1  3933  reusv2lem3  4537  fun11iun  5493  eusvobj2  6337  zfregcl  7308  scott0  7556  ac6c4  8108  lbzbi  10306  mreiincl  13498  lss1d  15720  isch3  21821  atom1d  22933  xrofsup  23255  esumc  23430  hasheuni  23453  esumcvg  23454  mptelee  24523  intopcoaconb  25540  bwt2  25592  indexa  26412  filbcmb  26432  sdclem1  26453  heibor1  26534  infrglb  27722  stoweidlem53  27802  stoweidlem57  27806  reuan  27958  2reurex  27959  2reu4a  27967  2reu7  27969  2reu8  27970  bnj900  28961  bnj1189  29039  bnj1204  29042  bnj1398  29064  bnj1444  29073  bnj1445  29074  bnj1446  29075  bnj1447  29076  bnj1467  29084  bnj1518  29094  bnj1519  29095  dihglblem5  31488
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-6 1703
This theorem depends on definitions:  df-bi 177  df-ex 1529  df-nf 1532  df-rex 2549
  Copyright terms: Public domain W3C validator