pwundif - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pwundif 2817

Description: Break up the power class of a union into a union of smaller classes.

**Assertion**
Ref	Expression
pwundif

**Proof of Theorem pwundif**
Step	Hyp	Ref	Expression
1		visset 1804	. . . 4
2	1	elpw 2394	. . 3
3		elun 2163	. . . 4 $\/$
4		eldif 2047	. . . . . 6 $/\$
5	1	elpw 2394	. . . . . . . 8
6	5	negbii 187	. . . . . . 7
7	2, 6	anbi12i 481	. . . . . 6 $/\$ $/\$
8	4, 7	bitr 173	. . . . 5 $/\$
9	8, 5	orbi12i 257	. . . 4 $\/$ $/\$ $\/$
10		ordir 595	. . . . 5 $/\$ $\/$ $\/$ $/\$ $\/$
11		pm2.1 654	. . . . . 6 $\/$
12	11	biantru 722	. . . . 5 $\/$ $\/$ $/\$ $\/$
13		id 59	. . . . . . 7
14		ssun3 2185	. . . . . . 7
15	13, 14	jaoi 341	. . . . . 6 $\/$
16		orc 269	. . . . . 6 $\/$
17	15, 16	impbi 157	. . . . 5 $\/$
18	10, 12, 17	3bitr2 179	. . . 4 $/\$ $\/$
19	3, 9, 18	3bitrr 178	. . 3
20	2, 19	bitr 173	. 2
21	20	eqriv 1467	1

Colors of variables: wff set class

Syntax hints:

wn 2 $\/$ wo 222 $/\$ wa 223

wceq 953

wcel 955

cdif 2034

cun 2035

wss 2037

cpw 2391

This theorem is referenced by: pwfilem 4544

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-12 965 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-clab 1457 df-cleq 1462 df-clel 1465 df-v 1803 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pw 2392