Theorem nfre1 2435

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

Step	Hyp	Ref	Expression
1		df-rex 2381	. 2 |- ( E. x e. A ph <-> E. x ( x e. A /\ ph ) )
2		nfe1 1440	. 2 |- F/ x E. x ( x e. A /\ ph )
3	1, 2	nfxfr 1418	1 |- F/ x E. x e. A ph

Syntax hints:   /\ wa 103   F/wnf 1404   E.wex 1436   e. wcel 1448   E.wrex 2376

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-ie1 1437

This theorem depends on definitions:  df-bi 116  df-nf 1405  df-rex 2381

This theorem is referenced by:  r19.29an  2532  nfiu1  3790  fun11iun  5322  eusvobj2  5692  fodjuomnilemdc  6928  prarloclem3step  7205  prmuloc2  7276  ltexprlemm  7309  caucvgprprlemaddq  7417  caucvgsrlemgt1  7490  supinfneg  9240  infsupneg  9241  lbzbi  9258  divalglemeunn  11413  divalglemeuneg  11415  bezoutlemmain  11479  bezout  11492  isomninnlem  12809