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

Theorem nfre1 2762
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 2711 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 nfe1 1777 . 2  |-  F/ x E. x ( x  e.  A  /\  ph )
31, 2nfxfr 1618 1  |-  F/ x E. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369   E.wex 1589   F/wnf 1592    e. wcel 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-10 1774
This theorem depends on definitions:  df-bi 185  df-ex 1590  df-nf 1593  df-rex 2711
This theorem is referenced by:  2rmorex  3152  nfiu1  4188  reusv2lem3  4483  eusvobj2  6072  fun11iun  6526  zfregcl  7797  scott0  8081  ac6c4  8638  lbzbi  10930  mreiincl  14516  lss1d  16965  neiptopnei  18577  neitr  18625  bwthOLD  18855  utopsnneiplem  19663  cfilucfilOLD  19985  cfilucfil  19986  restmetu  20003  colline  22917  f1otrg  22939  mptelee  22963  isch3  24466  atom1d  25579  xrofsup  25877  isarchi3  26027  ordtconlem1  26207  esumc  26358  hasheuni  26387  esumcvg  26388  voliune  26498  volfiniune  26499  ddemeas  26505  eulerpartlemgvv  26606  ptrest  28266  indexa  28468  filbcmb  28475  sdclem1  28480  heibor1  28550  infrglb  29614  stoweidlem53  29691  stoweidlem57  29695  reuan  29847  2reurex  29848  2reu4a  29856  2reu7  29858  2reu8  29859  bnj900  31621  bnj1189  31699  bnj1204  31702  bnj1398  31724  bnj1444  31733  bnj1445  31734  bnj1446  31735  bnj1447  31736  bnj1467  31744  bnj1518  31754  bnj1519  31755  dihglblem5  34513
  Copyright terms: Public domain W3C validator