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

Theorem nfre1 2612
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 2562 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 nfe1 1718 . 2  |-  F/ x E. x ( x  e.  A  /\  ph )
31, 2nfxfr 1560 1  |-  F/ x E. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 358   E.wex 1531   F/wnf 1534    e. wcel 1696   E.wrex 2557
This theorem is referenced by:  2rmorex  2982  nfiu1  3949  reusv2lem3  4553  fun11iun  5509  eusvobj2  6353  zfregcl  7324  scott0  7572  ac6c4  8124  lbzbi  10322  mreiincl  13514  lss1d  15736  isch3  21837  atom1d  22949  xrofsup  23270  esumc  23445  hasheuni  23468  esumcvg  23469  mptelee  24595  intopcoaconb  25643  bwt2  25695  indexa  26515  filbcmb  26535  sdclem1  26556  heibor1  26637  infrglb  27825  stoweidlem53  27905  stoweidlem57  27909  reuan  28061  2reurex  28062  2reu4a  28070  2reu7  28072  2reu8  28073  bnj900  29277  bnj1189  29355  bnj1204  29358  bnj1398  29380  bnj1444  29389  bnj1445  29390  bnj1446  29391  bnj1447  29392  bnj1467  29400  bnj1518  29410  bnj1519  29411  dihglblem5  32110
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-6 1715
This theorem depends on definitions:  df-bi 177  df-ex 1532  df-nf 1535  df-rex 2562
  Copyright terms: Public domain W3C validator