pwundif - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pwundif 2823

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 1809	. . . 4
2	1	elpw 2400	. . 3
3		elun 2169	. . . 4 $\/$
4		eldif 2053	. . . . . 6 $/\$
5	1	elpw 2400	. . . . . . . 8
6	5	negbii 187	. . . . . . 7
7	2, 6	anbi12i 482	. . . . . 6 $/\$ $/\$
8	4, 7	bitr 173	. . . . 5 $/\$
9	8, 5	orbi12i 257	. . . 4 $\/$ $/\$ $\/$
10		ordir 596	. . . . 5 $/\$ $\/$ $\/$ $/\$ $\/$
11		pm2.1 655	. . . . . 6 $\/$
12	11	biantru 723	. . . . 5 $\/$ $\/$ $/\$ $\/$
13		id 59	. . . . . . 7
14		ssun3 2191	. . . . . . 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 1472	1

Colors of variables: wff set class

Syntax hints:

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

wceq 954

wcel 956

cdif 2040

cun 2041

wss 2043

cpw 2397

This theorem is referenced by: pwfilem 4550

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-10 964 ax-12 966 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 979 df-sb 1170 df-clab 1462 df-cleq 1467 df-clel 1470 df-v 1808 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-pw 2398