tppreqb - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > tppreqb		Structured version Visualization version Unicode version

Theorem tppreqb 4336

Description: An unordered triple is an unordered pair if and only if one of its elements is a proper class or is identical with one of the another elements. (Contributed by Alexander van der Vekens, 15-Jan-2018.)

**Assertion**
Ref	Expression
tppreqb	$/\$ $/\$

**Proof of Theorem tppreqb**
Step	Hyp	Ref	Expression
1		3ianor 1055	. . . 4 $/\$ $/\$ $\/$ $\/$
2		df-3or 1038	. . . 4 $\/$ $\/$ $\/$ $\/$
3	1, 2	bitri 264	. . 3 $/\$ $/\$ $\/$ $\/$
4		orass 546	. . . . 5 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
5		ianor 509	. . . . . . . 8 $/\$ $\/$
6		tpprceq3 4335	. . . . . . . 8 $/\$
7	5, 6	sylbir 225	. . . . . . 7 $\/$
8		tpcoma 4285	. . . . . . 7
9		prcom 4267	. . . . . . 7
10	7, 8, 9	3eqtr3g 2679	. . . . . 6 $\/$
11		orcom 402	. . . . . . . 8 $\/$ $\/$
12		ianor 509	. . . . . . . 8 $/\$ $\/$
13	11, 12	bitr4i 267	. . . . . . 7 $\/$ $/\$
14		tpprceq3 4335	. . . . . . 7 $/\$
15	13, 14	sylbi 207	. . . . . 6 $\/$
16	10, 15	jaoi 394	. . . . 5 $\/$ $\/$ $\/$
17	4, 16	sylbi 207	. . . 4 $\/$ $\/$ $\/$
18	17	orcs 409	. . 3 $\/$ $\/$
19	3, 18	sylbi 207	. 2 $/\$ $/\$
20		df-tp 4182	. . . 4
21	20	eqeq1i 2627	. . 3
22		ssequn2 3786	. . . 4
23		snssg 4327	. . . . . . 7
24		elpri 4197	. . . . . . . 8 $\/$
25		nne 2798	. . . . . . . . . 10
26		3mix2 1231	. . . . . . . . . 10 $\/$ $\/$
27	25, 26	sylbir 225	. . . . . . . . 9 $\/$ $\/$
28		nne 2798	. . . . . . . . . 10
29		3mix3 1232	. . . . . . . . . 10 $\/$ $\/$
30	28, 29	sylbir 225	. . . . . . . . 9 $\/$ $\/$
31	27, 30	jaoi 394	. . . . . . . 8 $\/$ $\/$ $\/$
32	24, 31	syl 17	. . . . . . 7 $\/$ $\/$
33	23, 32	syl6bir 244	. . . . . 6 $\/$ $\/$
34		3mix1 1230	. . . . . . 7 $\/$ $\/$
35	34	a1d 25	. . . . . 6 $\/$ $\/$
36	33, 35	pm2.61i 176	. . . . 5 $\/$ $\/$
37	36, 1	sylibr 224	. . . 4 $/\$ $/\$
38	22, 37	sylbir 225	. . 3 $/\$ $/\$
39	21, 38	sylbi 207	. 2 $/\$ $/\$
40	19, 39	impbii 199	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

cvv 3200

cun 3572

wss 3574

csn 4177

cpr 4179

ctp 4181

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-sn 4178 df-pr 4180 df-tp 4182

This theorem is referenced by: (None)

W3C validator