Theorem 2ralunsn

Description: Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012)

	Ref	Expression
Hypotheses	2ralunsn.1	|- ( x = B -> ( ph <-> ch ) )
	2ralunsn.2	|- ( y = B -> ( ph <-> ps ) )
	2ralunsn.3	|- ( x = B -> ( ps <-> th ) )
Assertion	2ralunsn	|- ( B e. C -> ( A. x e. ( A u. { B } ) A. y e. ( A u. { B } ) ph <-> ( ( A. x e. A A. y e. A ph /\ A. x e. A ps ) /\ ( A. y e. A ch /\ th ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		2ralunsn.1	|- ( x = B -> ( ph <-> ch ) )
2		2ralunsn.2	|- ( y = B -> ( ph <-> ps ) )
3		2ralunsn.3	|- ( x = B -> ( ps <-> th ) )
4	2	ralunsn	|- ( B e. C -> ( A. y e. ( A u. { B } ) ph <-> ( A. y e. A ph /\ ps ) ) )
5	4	ralbidv	|- ( B e. C -> ( A. x e. ( A u. { B } ) A. y e. ( A u. { B } ) ph <-> A. x e. ( A u. { B } ) ( A. y e. A ph /\ ps ) ) )
6	1	ralbidv	|- ( x = B -> ( A. y e. A ph <-> A. y e. A ch ) )
7	6 3	anbi12d	|- ( x = B -> ( ( A. y e. A ph /\ ps ) <-> ( A. y e. A ch /\ th ) ) )
8	7	ralunsn	|- ( B e. C -> ( A. x e. ( A u. { B } ) ( A. y e. A ph /\ ps ) <-> ( A. x e. A ( A. y e. A ph /\ ps ) /\ ( A. y e. A ch /\ th ) ) ) )
9		r19.26	|- ( A. x e. A ( A. y e. A ph /\ ps ) <-> ( A. x e. A A. y e. A ph /\ A. x e. A ps ) )
10	9	anbi1i	|- ( ( A. x e. A ( A. y e. A ph /\ ps ) /\ ( A. y e. A ch /\ th ) ) <-> ( ( A. x e. A A. y e. A ph /\ A. x e. A ps ) /\ ( A. y e. A ch /\ th ) ) )
11	8 10	bitrdi	|- ( B e. C -> ( A. x e. ( A u. { B } ) ( A. y e. A ph /\ ps ) <-> ( ( A. x e. A A. y e. A ph /\ A. x e. A ps ) /\ ( A. y e. A ch /\ th ) ) ) )
12	5 11	bitrd	|- ( B e. C -> ( A. x e. ( A u. { B } ) A. y e. ( A u. { B } ) ph <-> ( ( A. x e. A A. y e. A ph /\ A. x e. A ps ) /\ ( A. y e. A ch /\ th ) ) ) )