Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem unopab 2121

Description: Union of two ordered pair class abstractions.

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

**Proof of Theorem unopab**
Step	Hyp	Ref	Expression
1		unab 1691	. . 3 $/\$ $/\$ $/\$ $\/$ $/\$
2		19.43 767	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
3		andi 456	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$ $/\$
4	3	biex 733	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$
5		19.43 767	. . . . . . 7 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
6	4, 5	bitr2 152	. . . . . 6 $/\$ $\/$ $/\$ $/\$ $\/$
7	6	biex 733	. . . . 5 $/\$ $\/$ $/\$ $/\$ $\/$
8	2, 7	bitr3 153	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$
9	8	biabi 1181	. . 3 $/\$ $\/$ $/\$ $/\$ $\/$
10	1, 9	eqtr 1119	. 2 $/\$ $/\$ $/\$ $\/$
11		df-opab 2098	. . 3 $/\$
12		df-opab 2098	. . 3 $/\$
13	11, 12	uneq12i 1609	. 2 $/\$ $/\$
14		df-opab 2098	. 2 $\/$ $/\$ $\/$
15	10, 13, 14	3eqtr4 1126	1 $\/$

Colors of variables: wff set class

Syntax hints: $\/$ wo 195 $/\$ wa 196

wex 678

cab 1090

wceq 1091

cun 1485

cop 1810

copab 2055

This theorem is referenced by: xpundi 2461 xpundir 2462

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-16 922 ax-17 925 ax-ext 1074

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-ex 679 df-sb 853 df-clab 1093 df-cleq 1097 df-clel 1099 df-v 1349 df-un 1490 df-opab 2098