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

Theorem nfre1 2706
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 2656 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 nfe1 1739 . 2  |-  F/ x E. x ( x  e.  A  /\  ph )
31, 2nfxfr 1576 1  |-  F/ x E. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1547   F/wnf 1550    e. wcel 1717   E.wrex 2651
This theorem is referenced by:  2rmorex  3082  nfiu1  4064  reusv2lem3  4667  fun11iun  5636  eusvobj2  6519  zfregcl  7496  scott0  7744  ac6c4  8295  lbzbi  10497  mreiincl  13749  lss1d  15967  neiptopnei  17120  neitr  17167  utopsnneiplem  18199  cfilucfil  18480  restmetu  18490  isch3  22593  atom1d  23705  xrofsup  23963  esumc  24243  hasheuni  24272  esumcvg  24273  voliune  24380  volfiniune  24381  mptelee  25549  indexa  26127  filbcmb  26134  sdclem1  26139  heibor1  26211  infrglb  27391  stoweidlem53  27471  stoweidlem57  27475  reuan  27627  2reurex  27628  2reu4a  27636  2reu7  27638  2reu8  27639  bnj900  28639  bnj1189  28717  bnj1204  28720  bnj1398  28742  bnj1444  28751  bnj1445  28752  bnj1446  28753  bnj1447  28754  bnj1467  28762  bnj1518  28772  bnj1519  28773  dihglblem5  31414
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-6 1736
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-rex 2656
  Copyright terms: Public domain W3C validator