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 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 2706
This theorem is referenced by:  2rmorex  3138  nfiu1  4121  reusv2lem3  4726  fun11iun  5695  eusvobj2  6582  zfregcl  7562  scott0  7810  ac6c4  8361  lbzbi  10564  mreiincl  13821  lss1d  16039  neiptopnei  17196  neitr  17244  bwth  17473  utopsnneiplem  18277  cfilucfilOLD  18599  cfilucfil  18600  restmetu  18617  isch3  22744  atom1d  23856  xrofsup  24126  esumc  24446  hasheuni  24475  esumcvg  24476  voliune  24585  volfiniune  24586  mptelee  25834  indexa  26435  filbcmb  26442  sdclem1  26447  heibor1  26519  infrglb  27698  stoweidlem53  27778  stoweidlem57  27782  reuan  27934  2reurex  27935  2reu4a  27943  2reu7  27945  2reu8  27946  bnj900  29300  bnj1189  29378  bnj1204  29381  bnj1398  29403  bnj1444  29412  bnj1445  29413  bnj1446  29414  bnj1447  29415  bnj1467  29423  bnj1518  29433  bnj1519  29434  dihglblem5  32096
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 2711
  Copyright terms: Public domain W3C validator