pwundif - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem pwundif 2828

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 1813	. . . 4
2	1	elpw 2404	. . 3
3		elun 2173	. . . 4 $\/$
4		eldif 2057	. . . . . 6 $/\$
5	1	elpw 2404	. . . . . . . 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 597	. . . . 5 $/\$ $\/$ $\/$ $/\$ $\/$
11		pm2.1 656	. . . . . 6 $\/$
12	11	biantru 724	. . . . 5 $\/$ $\/$ $/\$ $\/$
13		id 59	. . . . . . 7
14		ssun3 2195	. . . . . . 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 1474	1

Colors of variables: wff set class

Syntax hints:

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

wceq 956

wcel 958

cdif 2044

cun 2045

wss 2047

cpw 2401

This theorem is referenced by: pwfilemOLD 4570

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-10 966 ax-12 968 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 981 df-sb 1172 df-clab 1464 df-cleq 1469 df-clel 1472 df-v 1812 df-dif 2049 df-un 2050 df-in 2051 df-ss 2053 df-pw 2402