Theorem opeliunxp2

Description: Membership in a union of Cartesian products. (Contributed by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypothesis	opeliunxp2.1	|- ( x = C -> B = E )
Assertion	opeliunxp2	|- ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )

Proof

Step	Hyp	Ref	Expression
1		opeliunxp2.1	|- ( x = C -> B = E )
2		df-br	|- ( C U_ x e. A ( { x } X. B ) D <-> <. C , D >. e. U_ x e. A ( { x } X. B ) )
3		relxp	|- Rel ( { x } X. B )
4	3	rgenw	|- A. x e. A Rel ( { x } X. B )
5		reliun	|- ( Rel U_ x e. A ( { x } X. B ) <-> A. x e. A Rel ( { x } X. B ) )
6	4 5	mpbir	|- Rel U_ x e. A ( { x } X. B )
7	6	brrelex1i	|- ( C U_ x e. A ( { x } X. B ) D -> C e. _V )
8	2 7	sylbir	|- ( <. C , D >. e. U_ x e. A ( { x } X. B ) -> C e. _V )
9		elex	|- ( C e. A -> C e. _V )
10	9	adantr	|- ( ( C e. A /\ D e. E ) -> C e. _V )
11		nfiu1	|- F/_ x U_ x e. A ( { x } X. B )
12	11	nfel2	|- F/ x <. C , D >. e. U_ x e. A ( { x } X. B )
13		nfv	|- F/ x ( C e. A /\ D e. E )
14	12 13	nfbi	|- F/ x ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )
15		opeq1	|- ( x = C -> <. x , D >. = <. C , D >. )
16	15	eleq1d	|- ( x = C -> ( <. x , D >. e. U_ x e. A ( { x } X. B ) <-> <. C , D >. e. U_ x e. A ( { x } X. B ) ) )
17		eleq1	|- ( x = C -> ( x e. A <-> C e. A ) )
18	1	eleq2d	|- ( x = C -> ( D e. B <-> D e. E ) )
19	17 18	anbi12d	|- ( x = C -> ( ( x e. A /\ D e. B ) <-> ( C e. A /\ D e. E ) ) )
20	16 19	bibi12d	|- ( x = C -> ( ( <. x , D >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ D e. B ) ) <-> ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) ) ) )
21		opeliunxp	|- ( <. x , D >. e. U_ x e. A ( { x } X. B ) <-> ( x e. A /\ D e. B ) )
22	14 20 21	vtoclg1f	|- ( C e. _V -> ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) ) )
23	8 10 22	pm5.21nii	|- ( <. C , D >. e. U_ x e. A ( { x } X. B ) <-> ( C e. A /\ D e. E ) )