This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) ) )