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 32639

Description: The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3754. 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 3754 is undif3VD 32639 without virtual deductions and was automatically derived from undif3VD 32639.

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 3640	. . . . . 6 $\$ $\/$ $\$
2		eldif 3481	. . . . . . 7 $\$ $/\$
3	2	orbi2i 519	. . . . . 6 $\/$ $\$ $\/$ $/\$
4	1, 3	bitri 249	. . . . 5 $\$ $\/$ $/\$
5		idn1 32308	. . . . . . . . . 10
6		orc 385	. . . . . . . . . 10 $\/$
7	5, 6	e1a 32370	. . . . . . . . 9 $\/$
8		olc 384	. . . . . . . . . 10 $\/$
9	5, 8	e1a 32370	. . . . . . . . 9 $\/$
10		pm3.2 447	. . . . . . . . 9 $\/$ $\/$ $\/$ $/\$ $\/$
11	7, 9, 10	e11 32431	. . . . . . . 8 $\/$ $/\$ $\/$
12	11	in1 32305	. . . . . . 7 $\/$ $/\$ $\/$
13		idn1 32308	. . . . . . . . . . 11 $/\$ $/\$
14		simpl 457	. . . . . . . . . . 11 $/\$
15	13, 14	e1a 32370	. . . . . . . . . 10 $/\$
16		olc 384	. . . . . . . . . 10 $\/$
17	15, 16	e1a 32370	. . . . . . . . 9 $/\$ $\/$
18		simpr 461	. . . . . . . . . . 11 $/\$
19	13, 18	e1a 32370	. . . . . . . . . 10 $/\$
20		orc 385	. . . . . . . . . 10 $\/$
21	19, 20	e1a 32370	. . . . . . . . 9 $/\$ $\/$
22	17, 21, 10	e11 32431	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
23	22	in1 32305	. . . . . . 7 $/\$ $\/$ $/\$ $\/$
24	12, 23	jaoi 379	. . . . . 6 $\/$ $/\$ $\/$ $/\$ $\/$
25		anddi 866	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	25	bicomi 202	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
27		idn1 32308	. . . . . . . . . . 11 $/\$ $/\$
28		simpl 457	. . . . . . . . . . . 12 $/\$
29	28	orcd 392	. . . . . . . . . . 11 $/\$ $\/$ $/\$
30	27, 29	e1a 32370	. . . . . . . . . 10 $/\$ $\/$ $/\$
31	30	in1 32305	. . . . . . . . 9 $/\$ $\/$ $/\$
32		idn1 32308	. . . . . . . . . . . 12 $/\$ $/\$
33		simpl 457	. . . . . . . . . . . 12 $/\$
34	32, 33	e1a 32370	. . . . . . . . . . 11 $/\$
35		orc 385	. . . . . . . . . . 11 $\/$ $/\$
36	34, 35	e1a 32370	. . . . . . . . . 10 $/\$ $\/$ $/\$
37	36	in1 32305	. . . . . . . . 9 $/\$ $\/$ $/\$
38	31, 37	jaoi 379	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$ $/\$
39		olc 384	. . . . . . . . . . 11 $/\$ $\/$ $/\$
40	13, 39	e1a 32370	. . . . . . . . . 10 $/\$ $\/$ $/\$
41	40	in1 32305	. . . . . . . . 9 $/\$ $\/$ $/\$
42		idn1 32308	. . . . . . . . . . . 12 $/\$ $/\$
43		simpr 461	. . . . . . . . . . . 12 $/\$
44	42, 43	e1a 32370	. . . . . . . . . . 11 $/\$
45	44, 35	e1a 32370	. . . . . . . . . 10 $/\$ $\/$ $/\$
46	45	in1 32305	. . . . . . . . 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 3481	. . . . 5 $\$ $\$ $/\$ $\$
53		elun 3640	. . . . . 6 $\/$
54		eldif 3481	. . . . . . . 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 1596	. 2 $\$ $\$ $\$
62		dfcleq 2455	. . 3 $\$ $\$ $\$ $\$ $\$ $\$
63	62	biimpri 206	. 2 $\$ $\$ $\$ $\$ $\$ $\$
64	61, 63	e0a 32526	1 $\$ $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

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

wal 1372

wceq 1374

wcel 1762 $\$ cdif 3468

cun 3469

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1714 ax-7 1734 ax-10 1781 ax-11 1786 ax-12 1798 ax-13 1963 ax-ext 2440

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-tru 1377 df-ex 1592 df-nf 1595 df-sb 1707 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2612 df-v 3110 df-dif 3474 df-un 3476 df-vd1 32304

This theorem is referenced by: (None)

W3C validator