Theorem uniinqs 7448

Description: Class union distributes over the intersection of two subclasses of a quotient space. Compare uniin 4236. (Contributed by FL, 25-May-2007.) (Proof shortened by Mario Carneiro, 11-Jul-2014.)

Hypothesis

Ref	Expression
uniinqs.1	|- R Er X

Assertion

Ref	Expression
uniinqs	|- ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> U. ( B i^i C ) = ( U. B i^i U. C ) )

Proof of Theorem uniinqs

Dummy variables b c x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		uniin 4236	. . 3 |- U. ( B i^i C ) C_ ( U. B i^i U. C )
2	1	a1i 11	. 2 |- ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> U. ( B i^i C ) C_ ( U. B i^i U. C ) )
3		eluni2 4220	. . . . . 6 |- ( x e. U. B <-> E. b e. B x e. b )
4		eluni2 4220	. . . . . 6 |- ( x e. U. C <-> E. c e. C x e. c )
5	3, 4	anbi12i 701	. . . . 5 |- ( ( x e. U. B /\ x e. U. C ) <-> ( E. b e. B x e. b /\ E. c e. C x e. c ) )
6		elin 3649	. . . . 5 |- ( x e. ( U. B i^i U. C ) <-> ( x e. U. B /\ x e. U. C ) )
7		reeanv 2996	. . . . 5 |- ( E. b e. B E. c e. C ( x e. b /\ x e. c ) <-> ( E. b e. B x e. b /\ E. c e. C x e. c ) )
8	5, 6, 7	3bitr4i 280	. . . 4 |- ( x e. ( U. B i^i U. C ) <-> E. b e. B E. c e. C ( x e. b /\ x e. c ) )
9		simp3l 1033	. . . . . . 7 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> x e. b )
10		simp2l 1031	. . . . . . . 8 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b e. B )
11		inelcm 3847	. . . . . . . . . . 11 |- ( ( x e. b /\ x e. c ) -> ( b i^i c ) =/= (/) )
12	11	3ad2ant3 1028	. . . . . . . . . 10 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> ( b i^i c ) =/= (/) )
13		uniinqs.1	. . . . . . . . . . . . . 14 |- R Er X
14	13	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> R Er X )
15		simp1l 1029	. . . . . . . . . . . . . 14 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> B C_ ( A /. R ) )
16	15, 10	sseldd 3465	. . . . . . . . . . . . 13 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b e. ( A /. R ) )
17		simp1r 1030	. . . . . . . . . . . . . 14 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> C C_ ( A /. R ) )
18		simp2r 1032	. . . . . . . . . . . . . 14 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> c e. C )
19	17, 18	sseldd 3465	. . . . . . . . . . . . 13 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> c e. ( A /. R ) )
20	14, 16, 19	qsdisj 7445	. . . . . . . . . . . 12 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> ( b = c \/ ( b i^i c ) = (/) ) )
21	20	ord 378	. . . . . . . . . . 11 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> ( -. b = c -> ( b i^i c ) = (/) ) )
22	21	necon1ad 2640	. . . . . . . . . 10 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> ( ( b i^i c ) =/= (/) -> b = c ) )
23	12, 22	mpd 15	. . . . . . . . 9 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b = c )
24	23, 18	eqeltrd 2510	. . . . . . . 8 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b e. C )
25	10, 24	elind 3650	. . . . . . 7 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> b e. ( B i^i C ) )
26		elunii 4221	. . . . . . 7 |- ( ( x e. b /\ b e. ( B i^i C ) ) -> x e. U. ( B i^i C ) )
27	9, 25, 26	syl2anc 665	. . . . . 6 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) /\ ( x e. b /\ x e. c ) ) -> x e. U. ( B i^i C ) )
28	27	3expia 1207	. . . . 5 |- ( ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) /\ ( b e. B /\ c e. C ) ) -> ( ( x e. b /\ x e. c ) -> x e. U. ( B i^i C ) ) )
29	28	rexlimdvva 2924	. . . 4 |- ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> ( E. b e. B E. c e. C ( x e. b /\ x e. c ) -> x e. U. ( B i^i C ) ) )
30	8, 29	syl5bi 220	. . 3 |- ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> ( x e. ( U. B i^i U. C ) -> x e. U. ( B i^i C ) ) )
31	30	ssrdv 3470	. 2 |- ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> ( U. B i^i U. C ) C_ U. ( B i^i C ) )
32	2, 31	eqssd 3481	1 |- ( ( B C_ ( A /. R ) /\ C C_ ( A /. R ) ) -> U. ( B i^i C ) = ( U. B i^i U. C ) )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982   = wceq 1437   e. wcel 1868   =/= wne 2618   E.wrex 2776   i^i cin 3435   C_ wss 3436   (/)c0 3761   U.cuni 4216   Er wer 7365   /.cqs 7367

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4552  ax-pr 4657

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-br 4421  df-opab 4480  df-xp 4856  df-rel 4857  df-cnv 4858  df-co 4859  df-dm 4860  df-rn 4861  df-res 4862  df-ima 4863  df-er 7368  df-ec 7370  df-qs 7374

This theorem is referenced by: (None)