Theorem ceqsrexv

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by NM, 30-Apr-2004)

	Ref	Expression
Hypothesis	ceqsrexv.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	ceqsrexv	|- ( A e. B -> ( E. x e. B ( x = A /\ ph ) <-> ps ) )

Proof

Step	Hyp	Ref	Expression
1		ceqsrexv.1	|- ( x = A -> ( ph <-> ps ) )
2		df-rex	|- ( E. x e. B ( x = A /\ ph ) <-> E. x ( x e. B /\ ( x = A /\ ph ) ) )
3		an12	|- ( ( x = A /\ ( x e. B /\ ph ) ) <-> ( x e. B /\ ( x = A /\ ph ) ) )
4	3	exbii	|- ( E. x ( x = A /\ ( x e. B /\ ph ) ) <-> E. x ( x e. B /\ ( x = A /\ ph ) ) )
5	2 4	bitr4i	|- ( E. x e. B ( x = A /\ ph ) <-> E. x ( x = A /\ ( x e. B /\ ph ) ) )
6		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
7	6 1	anbi12d	|- ( x = A -> ( ( x e. B /\ ph ) <-> ( A e. B /\ ps ) ) )
8	7	ceqsexgv	|- ( A e. B -> ( E. x ( x = A /\ ( x e. B /\ ph ) ) <-> ( A e. B /\ ps ) ) )
9	8	bianabs	|- ( A e. B -> ( E. x ( x = A /\ ( x e. B /\ ph ) ) <-> ps ) )
10	5 9	bitrid	|- ( A e. B -> ( E. x e. B ( x = A /\ ph ) <-> ps ) )