tpres - Metamath Proof Explorer

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

Theorem tpres 6466

Description: An unordered triple of ordered pairs restricted to all but one first components of the pairs is an unordered pair of ordered pairs. (Contributed by AV, 14-Mar-2020.)

**Hypotheses**
Ref	Expression
tpres.t
tpres.b
tpres.c
tpres.e
tpres.f
tpres.1
tpres.2

**Assertion**
Ref	Expression
tpres	$\$

Proof of Theorem tpres Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-res 5126	. 2 $\$ $\$
2		elin 3796	. . . 4 $\$ $/\$ $\$
3		elxp 5131	. . . . . 6 $\$ $/\$ $\$ $/\$
4	3	anbi2i 730	. . . . 5 $/\$ $\$ $/\$ $/\$ $\$ $/\$
5		tpres.t	. . . . . . . . 9
6	5	eleq2d 2687	. . . . . . . 8
7		vex 3203	. . . . . . . . . . . . 13
8	7	eltp 4230	. . . . . . . . . . . 12 $\/$ $\/$
9		eldifsn 4317	. . . . . . . . . . . . . . . . . . . 20 $\$ $/\$
10		eqeq1 2626	. . . . . . . . . . . . . . . . . . . . . . . . 25
11	10	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
12		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
13		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
14	12, 13	opth 4945	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
15		eqneqall 2805	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $\/$
16	15	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $\/$
17	16	impd 447	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $\/$
18	14, 17	syl5bi 232	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\/$
19	18	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\/$
20	11, 19	sylbid 230	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\/$
21	20	impd 447	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$
22	21	ex 450	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\/$
23	22	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $\/$
24	9, 23	sylbi 207	. . . . . . . . . . . . . . . . . . 19 $\$ $/\$ $\/$
25	24	adantr 481	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $/\$ $\/$
26	25	impcom 446	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $/\$ $\/$
27	26	com12 32	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $/\$ $\/$
28	27	exlimdvv 1862	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $/\$ $\/$
29	28	ex 450	. . . . . . . . . . . . . 14 $/\$ $\$ $/\$ $\/$
30	29	impd 447	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\/$
31		orc 400	. . . . . . . . . . . . . 14 $\/$
32	31	a1d 25	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\/$
33		olc 399	. . . . . . . . . . . . . 14 $\/$
34	33	a1d 25	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $/\$ $\/$
35	30, 32, 34	3jaoi 1391	. . . . . . . . . . . 12 $\/$ $\/$ $/\$ $/\$ $\$ $/\$ $\/$
36	8, 35	sylbi 207	. . . . . . . . . . 11 $/\$ $/\$ $\$ $/\$ $\/$
37	7	elpr 4198	. . . . . . . . . . 11 $\/$
38	36, 37	syl6ibr 242	. . . . . . . . . 10 $/\$ $/\$ $\$ $/\$
39	38	expd 452	. . . . . . . . 9 $/\$ $\$ $/\$
40	39	com12 32	. . . . . . . 8 $/\$ $\$ $/\$
41	6, 40	sylbid 230	. . . . . . 7 $/\$ $\$ $/\$
42	41	impd 447	. . . . . 6 $/\$ $/\$ $\$ $/\$
43		3mix2 1231	. . . . . . . . . . . . 13 $\/$ $\/$
44		3mix3 1232	. . . . . . . . . . . . 13 $\/$ $\/$
45	43, 44	jaoi 394	. . . . . . . . . . . 12 $\/$ $\/$ $\/$
46	45	adantr 481	. . . . . . . . . . 11 $\/$ $/\$ $\/$ $\/$
47	6, 8	syl6bb 276	. . . . . . . . . . . 12 $\/$ $\/$
48	47	adantl 482	. . . . . . . . . . 11 $\/$ $/\$ $\/$ $\/$
49	46, 48	mpbird 247	. . . . . . . . . 10 $\/$ $/\$
50		tpres.b	. . . . . . . . . . . . . . . 16
51		elex 3212	. . . . . . . . . . . . . . . 16
52	50, 51	syl 17	. . . . . . . . . . . . . . 15
53		tpres.1	. . . . . . . . . . . . . . 15
54		tpres.e	. . . . . . . . . . . . . . . 16
55		elex 3212	. . . . . . . . . . . . . . . 16
56	54, 55	syl 17	. . . . . . . . . . . . . . 15
57	52, 53, 56	jca31 557	. . . . . . . . . . . . . 14 $/\$ $/\$
58	57	anim2i 593	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
59		opeq12 4404	. . . . . . . . . . . . . . . . . 18 $/\$
60	59	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 $/\$
61		eleq1 2689	. . . . . . . . . . . . . . . . . . 19
62		neeq1 2856	. . . . . . . . . . . . . . . . . . 19
63	61, 62	anbi12d 747	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
64		eleq1 2689	. . . . . . . . . . . . . . . . . 18
65	63, 64	bi2anan9 917	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
66	60, 65	anbi12d 747	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
67	66	spc2egv 3295	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
68	50, 54, 67	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
69	68	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
70	58, 69	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
71		tpres.c	. . . . . . . . . . . . . . . 16
72		elex 3212	. . . . . . . . . . . . . . . 16
73	71, 72	syl 17	. . . . . . . . . . . . . . 15
74		tpres.2	. . . . . . . . . . . . . . 15
75		tpres.f	. . . . . . . . . . . . . . . 16
76		elex 3212	. . . . . . . . . . . . . . . 16
77	75, 76	syl 17	. . . . . . . . . . . . . . 15
78	73, 74, 77	jca31 557	. . . . . . . . . . . . . 14 $/\$ $/\$
79	78	anim2i 593	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$
80		opeq12 4404	. . . . . . . . . . . . . . . . . 18 $/\$
81	80	eqeq2d 2632	. . . . . . . . . . . . . . . . 17 $/\$
82		eleq1 2689	. . . . . . . . . . . . . . . . . . 19
83		neeq1 2856	. . . . . . . . . . . . . . . . . . 19
84	82, 83	anbi12d 747	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
85		eleq1 2689	. . . . . . . . . . . . . . . . . 18
86	84, 85	bi2anan9 917	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ $/\$ $/\$
87	81, 86	anbi12d 747	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
88	87	spc2egv 3295	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
89	71, 75, 88	syl2anc 693	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
90	89	adantl 482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
91	79, 90	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
92	70, 91	jaoian 824	. . . . . . . . . . 11 $\/$ $/\$ $/\$ $/\$ $/\$
93	9	anbi1i 731	. . . . . . . . . . . . 13 $\$ $/\$ $/\$ $/\$
94	93	anbi2i 730	. . . . . . . . . . . 12 $/\$ $\$ $/\$ $/\$ $/\$ $/\$
95	94	2exbii 1775	. . . . . . . . . . 11 $/\$ $\$ $/\$ $/\$ $/\$ $/\$
96	92, 95	sylibr 224	. . . . . . . . . 10 $\/$ $/\$ $/\$ $\$ $/\$
97	49, 96	jca 554	. . . . . . . . 9 $\/$ $/\$ $/\$ $/\$ $\$ $/\$
98	97	ex 450	. . . . . . . 8 $\/$ $/\$ $/\$ $\$ $/\$
99	37, 98	sylbi 207	. . . . . . 7 $/\$ $/\$ $\$ $/\$
100	99	com12 32	. . . . . 6 $/\$ $/\$ $\$ $/\$
101	42, 100	impbid 202	. . . . 5 $/\$ $/\$ $\$ $/\$
102	4, 101	syl5bb 272	. . . 4 $/\$ $\$
103	2, 102	syl5bb 272	. . 3 $\$
104	103	eqrdv 2620	. 2 $\$
105	1, 104	syl5eq 2668	1 $\$

Colors of variables: wff setvar class

Syntax hints:

wi 4

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

wceq 1483

wex 1704

wcel 1990

wne 2794

cvv 3200 $\$ cdif 3571

cin 3573

csn 4177

cpr 4179

ctp 4181

cop 4183

cxp 5112

cres 5116

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 ax-sep 4781 ax-nul 4789 ax-pr 4906

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-rab 2921 df-v 3202 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-opab 4713 df-xp 5120 df-res 5126

This theorem is referenced by: estrres 16779

W3C validator