Theorem ceqsrexbv

Description: Elimination of a restricted existential quantifier, using implicit substitution. (Contributed by Mario Carneiro, 14-Mar-2014)

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

Proof

Step	Hyp	Ref	Expression
1		ceqsrexv.1	|- ( x = A -> ( ph <-> ps ) )
2		r19.42v	|- ( E. x e. B ( A e. B /\ ( x = A /\ ph ) ) <-> ( A e. B /\ E. x e. B ( x = A /\ ph ) ) )
3		eleq1	|- ( x = A -> ( x e. B <-> A e. B ) )
4	3	adantr	|- ( ( x = A /\ ph ) -> ( x e. B <-> A e. B ) )
5	4	pm5.32ri	|- ( ( x e. B /\ ( x = A /\ ph ) ) <-> ( A e. B /\ ( x = A /\ ph ) ) )
6	5	bicomi	|- ( ( A e. B /\ ( x = A /\ ph ) ) <-> ( x e. B /\ ( x = A /\ ph ) ) )
7	6	baib	|- ( x e. B -> ( ( A e. B /\ ( x = A /\ ph ) ) <-> ( x = A /\ ph ) ) )
8	7	rexbiia	|- ( E. x e. B ( A e. B /\ ( x = A /\ ph ) ) <-> E. x e. B ( x = A /\ ph ) )
9	1	ceqsrexv	|- ( A e. B -> ( E. x e. B ( x = A /\ ph ) <-> ps ) )
10	9	pm5.32i	|- ( ( A e. B /\ E. x e. B ( x = A /\ ph ) ) <-> ( A e. B /\ ps ) )
11	2 8 10	3bitr3i	|- ( E. x e. B ( x = A /\ ph ) <-> ( A e. B /\ ps ) )