Theorem rexbidar

Description: More general form of rexbida . (Contributed by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Hypotheses	ralbidar.1	|- ( ph -> A. x e. A ph )
	ralbidar.2	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
Assertion	rexbidar	|- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Proof

Step	Hyp	Ref	Expression
1		ralbidar.1	|- ( ph -> A. x e. A ph )
2		ralbidar.2	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	2	ex	|- ( ph -> ( x e. A -> ( ps <-> ch ) ) )
4	3	ralimi	|- ( A. x e. A ph -> A. x e. A ( x e. A -> ( ps <-> ch ) ) )
5	1 4	syl	|- ( ph -> A. x e. A ( x e. A -> ( ps <-> ch ) ) )
6		df-ral	|- ( A. x e. A ( x e. A -> ( ps <-> ch ) ) <-> A. x ( x e. A -> ( x e. A -> ( ps <-> ch ) ) ) )
7	5 6	sylib	|- ( ph -> A. x ( x e. A -> ( x e. A -> ( ps <-> ch ) ) ) )
8		pm2.43	|- ( ( x e. A -> ( x e. A -> ( ps <-> ch ) ) ) -> ( x e. A -> ( ps <-> ch ) ) )
9	8	pm5.32d	|- ( ( x e. A -> ( x e. A -> ( ps <-> ch ) ) ) -> ( ( x e. A /\ ps ) <-> ( x e. A /\ ch ) ) )
10	9	alimi	|- ( A. x ( x e. A -> ( x e. A -> ( ps <-> ch ) ) ) -> A. x ( ( x e. A /\ ps ) <-> ( x e. A /\ ch ) ) )
11		exbi	|- ( A. x ( ( x e. A /\ ps ) <-> ( x e. A /\ ch ) ) -> ( E. x ( x e. A /\ ps ) <-> E. x ( x e. A /\ ch ) ) )
12	7 10 11	3syl	|- ( ph -> ( E. x ( x e. A /\ ps ) <-> E. x ( x e. A /\ ch ) ) )
13		df-rex	|- ( E. x e. A ps <-> E. x ( x e. A /\ ps ) )
14		df-rex	|- ( E. x e. A ch <-> E. x ( x e. A /\ ch ) )
15	12 13 14	3bitr4g	|- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )