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

Theorem nfre1 2754
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 2703 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 nfe1 1747 . 2  |-  F/ x E. x ( x  e.  A  /\  ph )
31, 2nfxfr 1579 1  |-  F/ x E. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    /\ wa 359   E.wex 1550   F/wnf 1553    e. wcel 1725   E.wrex 2698
This theorem is referenced by:  2rmorex  3130  nfiu1  4113  reusv2lem3  4717  fun11iun  5686  eusvobj2  6573  zfregcl  7551  scott0  7799  ac6c4  8350  lbzbi  10553  mreiincl  13809  lss1d  16027  neiptopnei  17184  neitr  17232  bwth  17461  utopsnneiplem  18265  cfilucfilOLD  18587  cfilucfil  18588  restmetu  18605  isch3  22732  atom1d  23844  xrofsup  24114  esumc  24434  hasheuni  24463  esumcvg  24464  voliune  24573  volfiniune  24574  mptelee  25782  indexa  26372  filbcmb  26379  sdclem1  26384  heibor1  26456  infrglb  27636  stoweidlem53  27716  stoweidlem57  27720  reuan  27872  2reurex  27873  2reu4a  27881  2reu7  27883  2reu8  27884  bnj900  29154  bnj1189  29232  bnj1204  29235  bnj1398  29257  bnj1444  29266  bnj1445  29267  bnj1446  29268  bnj1447  29269  bnj1467  29277  bnj1518  29287  bnj1519  29288  dihglblem5  31935
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-6 1744
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-nf 1554  df-rex 2703
  Copyright terms: Public domain W3C validator