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

Theorem nfre1 2915
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 2810 . 2  |-  ( E. x  e.  A  ph  <->  E. x ( x  e.  A  /\  ph )
)
2 nfe1 1845 . 2  |-  F/ x E. x ( x  e.  A  /\  ph )
31, 2nfxfr 1650 1  |-  F/ x E. x  e.  A  ph
Colors of variables: wff setvar class
Syntax hints:    /\ wa 367   E.wex 1617   F/wnf 1621    e. wcel 1823   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-10 1842
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622  df-rex 2810
This theorem is referenced by:  r19.29an  2995  2rmorex  3301  nfiu1  4345  reusv2lem3  4640  eusvobj2  6263  fun11iun  6733  zfregcl  8012  scott0  8295  ac6c4  8852  lbzbi  11171  mreiincl  15085  lss1d  17804  neiptopnei  19800  neitr  19848  utopsnneiplem  20916  cfilucfilOLD  21238  cfilucfil  21239  mptelee  24400  isch3  26357  atom1d  27470  elsnxp  27684  xrofsup  27816  2sqmo  27871  locfinreflem  28078  esumc  28280  esumrnmpt2  28297  hasheuni  28314  esumcvg  28315  esumcvgre  28320  voliune  28438  volfiniune  28439  ddemeas  28445  eulerpartlemgvv  28579  ptrest  30288  indexa  30464  filbcmb  30471  sdclem1  30476  heibor1  30546  suprnmpt  31691  upbdrech  31744  ssfiunibd  31748  iccshift  31797  iooshift  31801  infrglb  31823  islpcn  31884  limsupre  31886  limclner  31896  itgperiod  32019  stoweidlem53  32074  stoweidlem57  32078  fourierdlem48  32176  fourierdlem51  32179  fourierdlem73  32201  fourierdlem81  32209  elaa2  32256  etransclem32  32288  reuan  32424  2reurex  32425  2reu4a  32433  2reu7  32435  2reu8  32436  2zrngagrp  33003  2zrngmmgm  33006  bnj900  34388  bnj1189  34466  bnj1204  34469  bnj1398  34491  bnj1444  34500  bnj1445  34501  bnj1446  34502  bnj1447  34503  bnj1467  34511  bnj1518  34521  bnj1519  34522  dihglblem5  37422
  Copyright terms: Public domain W3C validator