Theorem ralbidar

Description: More general form of ralbida . (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	ralbidar	|- ( ph -> ( A. x e. A ps <-> A. 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.74d	|- ( ( 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		albi	|- ( A. x ( ( x e. A -> ps ) <-> ( x e. A -> ch ) ) -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. A -> ch ) ) )
12	7 10 11	3syl	|- ( ph -> ( A. x ( x e. A -> ps ) <-> A. x ( x e. A -> ch ) ) )
13		df-ral	|- ( A. x e. A ps <-> A. x ( x e. A -> ps ) )
14		df-ral	|- ( A. x e. A ch <-> A. x ( x e. A -> ch ) )
15	12 13 14	3bitr4g	|- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )