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

Theorem nfre1 2764
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 2713 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 nfe1 1748 . 2  |-  F/ x E. x ( x  e.  A  /\  ph )
31, 2nfxfr 1580 1  |-  F/ x E. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1551   F/wnf 1554    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  2rmorex  3140  nfiu1  4123  reusv2lem3  4729  fun11iun  5698  eusvobj2  6585  zfregcl  7565  scott0  7815  ac6c4  8366  lbzbi  10569  mreiincl  13826  lss1d  16044  neiptopnei  17201  neitr  17249  bwth  17478  utopsnneiplem  18282  cfilucfilOLD  18604  cfilucfil  18605  restmetu  18622  isch3  22749  atom1d  23861  xrofsup  24131  esumc  24451  hasheuni  24480  esumcvg  24481  voliune  24590  volfiniune  24591  mptelee  25839  indexa  26449  filbcmb  26456  sdclem1  26461  heibor1  26533  infrglb  27712  stoweidlem53  27792  stoweidlem57  27796  reuan  27948  2reurex  27949  2reu4a  27957  2reu7  27959  2reu8  27960  bnj900  29374  bnj1189  29452  bnj1204  29455  bnj1398  29477  bnj1444  29486  bnj1445  29487  bnj1446  29488  bnj1447  29489  bnj1467  29497  bnj1518  29507  bnj1519  29508  dihglblem5  32170
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-6 1745
This theorem depends on definitions:  df-bi 179  df-ex 1552  df-nf 1555  df-rex 2713
  Copyright terms: Public domain W3C validator