unopab - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > unopab		Unicode version

Theorem unopab 4162

Description: Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002.)

**Assertion**
Ref	Expression
unopab	$\/$

Proof of Theorem unopab Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		unab 3471	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$
2		19.43 1674	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
3		andi 823	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$ $/\$
4	3	exbii 1651	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$
5		19.43 1674	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
6	4, 5	bitr2i 185	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$
7	6	exbii 1651	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$
8	2, 7	bitr3i 186	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$
9	8	abbii 2345	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$
10	1, 9	eqtri 2250	. 2 $/\$ $/\$ $/\$ $\/$
11		df-opab 4145	. . 3 $/\$
12		df-opab 4145	. . 3 $/\$
13	11, 12	uneq12i 3356	. 2 $/\$ $/\$
14		df-opab 4145	. 2 $\/$ $/\$ $\/$
15	10, 13, 14	3eqtr4i 2260	1 $\/$

Colors of variables: wff set class

Syntax hints: $/\$ wa 104 $\/$ wo 713

wceq 1395

wex 1538

cab 2215

cun 3195

cop 3669

copab 4143

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-ext 2211

This theorem depends on definitions: df-bi 117 df-tru 1398 df-nf 1507 df-sb 1809 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-v 2801 df-un 3201 df-opab 4145

This theorem is referenced by: xpundi 4774 xpundir 4775 cnvun 5133 coundi 5229 coundir 5230 mptun 5454 lgsquadlem3 15752