undif3VD - Mathbox for Alan Sare

	Mathbox for Alan Sare	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > undif3VD		Structured version Unicode version

Theorem undif3VD 33415

Description: The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3744. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. undif3 3744 is undif3VD 33415 without virtual deductions and was automatically derived from undif3VD 33415.

1::	$\$ $\/$ $\$
2::	$\$ $/\$
3:2:	$\/$ $\$ $\/$ $/\$
4:1,3:	$\$ $\/$ $/\$
5::
6:5:	$\/$
7:5:	$\/$
8:6,7:	$\/$ $/\$ $\/$
9:8:	$\/$ $/\$ $\/$
10::	$/\$ $/\$
11:10:	$/\$
12:10:	$/\$
13:11:	$/\$ $\/$
14:12:	$/\$ $\/$
15:13,14:	$/\$ $\/$ $/\$ $\/$
16:15:	$/\$ $\/$ $/\$ $\/$
17:9,16:	$\/$ $/\$ $\/$ $/\$ $\/$
18::	$/\$ $/\$
19:18:	$/\$
20:18:	$/\$
21:18:	$/\$ $\/$ $/\$
22:21:	$/\$ $\/$ $/\$
23::	$/\$ $/\$
24:23:	$/\$
25:24:	$/\$ $\/$ $/\$
26:25:	$/\$ $\/$ $/\$
27:10:	$/\$ $\/$ $/\$
28:27:	$/\$ $\/$ $/\$
29::	$/\$ $/\$
30:29:	$/\$
31:30:	$/\$ $\/$ $/\$
32:31:	$/\$ $\/$ $/\$
33:22,26:	$/\$ $\/$ $/\$ $\/$ $/\$
34:28,32:	$/\$ $\/$ $/\$ $\/$ $/\$
35:33,34:	$/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
36::	$/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
37:36,35:	$\/$ $/\$ $\/$ $\/$ $/\$
38:17,37:	$\/$ $/\$ $\/$ $/\$ $\/$
39::	$\$ $/\$
40:39:	$\$ $/\$
41::	$/\$ $\/$
42:40,41:	$\$ $\/$
43::	$\/$
44:43,42:	$/\$ $\$ $\/$ $/\$ $/\$
45::	$\$ $\$ $/\$ $\$
46:45,44:	$\$ $\$ $\/$ $/\$ $\/$
47:4,38:	$\$ $\/$ $/\$ $\/$
48:46,47:	$\$ $\$ $\$
49:48:	$\$ $\$ $\$
qed:49:	$\$ $\$ $\$

(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
undif3VD	$\$ $\$ $\$

Proof of Theorem undif3VD Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elun 3630	. . . . . 6 $\$ $\/$ $\$
2		eldif 3471	. . . . . . 7 $\$ $/\$
3	2	orbi2i 519	. . . . . 6 $\/$ $\$ $\/$ $/\$
4	1, 3	bitri 249	. . . . 5 $\$ $\/$ $/\$
5		idn1 33084	. . . . . . . . . 10
6		orc 385	. . . . . . . . . 10 $\/$
7	5, 6	e1a 33146	. . . . . . . . 9 $\/$
8		olc 384	. . . . . . . . . 10 $\/$
9	5, 8	e1a 33146	. . . . . . . . 9 $\/$
10		pm3.2 447	. . . . . . . . 9 $\/$ $\/$ $\/$ $/\$ $\/$
11	7, 9, 10	e11 33207	. . . . . . . 8 $\/$ $/\$ $\/$
12	11	in1 33081	. . . . . . 7 $\/$ $/\$ $\/$
13		idn1 33084	. . . . . . . . . . 11 $/\$ $/\$
14		simpl 457	. . . . . . . . . . 11 $/\$
15	13, 14	e1a 33146	. . . . . . . . . 10 $/\$
16		olc 384	. . . . . . . . . 10 $\/$
17	15, 16	e1a 33146	. . . . . . . . 9 $/\$ $\/$
18		simpr 461	. . . . . . . . . . 11 $/\$
19	13, 18	e1a 33146	. . . . . . . . . 10 $/\$
20		orc 385	. . . . . . . . . 10 $\/$
21	19, 20	e1a 33146	. . . . . . . . 9 $/\$ $\/$
22	17, 21, 10	e11 33207	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
23	22	in1 33081	. . . . . . 7 $/\$ $\/$ $/\$ $\/$
24	12, 23	jaoi 379	. . . . . 6 $\/$ $/\$ $\/$ $/\$ $\/$
25		anddi 870	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	25	bicomi 202	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
27		idn1 33084	. . . . . . . . . . 11 $/\$ $/\$
28		simpl 457	. . . . . . . . . . . 12 $/\$
29	28	orcd 392	. . . . . . . . . . 11 $/\$ $\/$ $/\$
30	27, 29	e1a 33146	. . . . . . . . . 10 $/\$ $\/$ $/\$
31	30	in1 33081	. . . . . . . . 9 $/\$ $\/$ $/\$
32		idn1 33084	. . . . . . . . . . . 12 $/\$ $/\$
33		simpl 457	. . . . . . . . . . . 12 $/\$
34	32, 33	e1a 33146	. . . . . . . . . . 11 $/\$
35		orc 385	. . . . . . . . . . 11 $\/$ $/\$
36	34, 35	e1a 33146	. . . . . . . . . 10 $/\$ $\/$ $/\$
37	36	in1 33081	. . . . . . . . 9 $/\$ $\/$ $/\$
38	31, 37	jaoi 379	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$ $/\$
39		olc 384	. . . . . . . . . . 11 $/\$ $\/$ $/\$
40	13, 39	e1a 33146	. . . . . . . . . 10 $/\$ $\/$ $/\$
41	40	in1 33081	. . . . . . . . 9 $/\$ $\/$ $/\$
42		idn1 33084	. . . . . . . . . . . 12 $/\$ $/\$
43		simpr 461	. . . . . . . . . . . 12 $/\$
44	42, 43	e1a 33146	. . . . . . . . . . 11 $/\$
45	44, 35	e1a 33146	. . . . . . . . . 10 $/\$ $\/$ $/\$
46	45	in1 33081	. . . . . . . . 9 $/\$ $\/$ $/\$
47	41, 46	jaoi 379	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$ $/\$
48	38, 47	jaoi 379	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
49	26, 48	sylbir 213	. . . . . 6 $\/$ $/\$ $\/$ $\/$ $/\$
50	24, 49	impbii 188	. . . . 5 $\/$ $/\$ $\/$ $/\$ $\/$
51	4, 50	bitri 249	. . . 4 $\$ $\/$ $/\$ $\/$
52		eldif 3471	. . . . 5 $\$ $\$ $/\$ $\$
53		elun 3630	. . . . . 6 $\/$
54		eldif 3471	. . . . . . . 8 $\$ $/\$
55	54	notbii 296	. . . . . . 7 $\$ $/\$
56		pm4.53 492	. . . . . . 7 $/\$ $\/$
57	55, 56	bitri 249	. . . . . 6 $\$ $\/$
58	53, 57	anbi12i 697	. . . . 5 $/\$ $\$ $\/$ $/\$ $\/$
59	52, 58	bitri 249	. . . 4 $\$ $\$ $\/$ $/\$ $\/$
60	51, 59	bitr4i 252	. . 3 $\$ $\$ $\$
61	60	ax-gen 1605	. 2 $\$ $\$ $\$
62		dfcleq 2436	. . 3 $\$ $\$ $\$ $\$ $\$ $\$
63	62	biimpri 206	. 2 $\$ $\$ $\$ $\$ $\$ $\$
64	61, 63	e0a 33302	1 $\$ $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 184 $\/$ wo 368 $/\$ wa 369

wal 1381

wceq 1383

wcel 1804 $\$ cdif 3458

cun 3459

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-v 3097 df-dif 3464 df-un 3466 df-vd1 33080

This theorem is referenced by: (None)

W3C validator