undif3VD - Mathbox for Alan Sare

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

Theorem undif3VD 37279

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

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 3574	. . . . . 6 $\$ $\/$ $\$
2		eldif 3414	. . . . . . 7 $\$ $/\$
3	2	orbi2i 522	. . . . . 6 $\/$ $\$ $\/$ $/\$
4	1, 3	bitri 253	. . . . 5 $\$ $\/$ $/\$
5		idn1 36944	. . . . . . . . . 10
6		orc 387	. . . . . . . . . 10 $\/$
7	5, 6	e1a 37006	. . . . . . . . 9 $\/$
8		olc 386	. . . . . . . . . 10 $\/$
9	5, 8	e1a 37006	. . . . . . . . 9 $\/$
10		pm3.2 449	. . . . . . . . 9 $\/$ $\/$ $\/$ $/\$ $\/$
11	7, 9, 10	e11 37067	. . . . . . . 8 $\/$ $/\$ $\/$
12	11	in1 36941	. . . . . . 7 $\/$ $/\$ $\/$
13		idn1 36944	. . . . . . . . . . 11 $/\$ $/\$
14		simpl 459	. . . . . . . . . . 11 $/\$
15	13, 14	e1a 37006	. . . . . . . . . 10 $/\$
16		olc 386	. . . . . . . . . 10 $\/$
17	15, 16	e1a 37006	. . . . . . . . 9 $/\$ $\/$
18		simpr 463	. . . . . . . . . . 11 $/\$
19	13, 18	e1a 37006	. . . . . . . . . 10 $/\$
20		orc 387	. . . . . . . . . 10 $\/$
21	19, 20	e1a 37006	. . . . . . . . 9 $/\$ $\/$
22	17, 21, 10	e11 37067	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$
23	22	in1 36941	. . . . . . 7 $/\$ $\/$ $/\$ $\/$
24	12, 23	jaoi 381	. . . . . 6 $\/$ $/\$ $\/$ $/\$ $\/$
25		anddi 881	. . . . . . . 8 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
26	25	bicomi 206	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
27		idn1 36944	. . . . . . . . . . 11 $/\$ $/\$
28		simpl 459	. . . . . . . . . . . 12 $/\$
29	28	orcd 394	. . . . . . . . . . 11 $/\$ $\/$ $/\$
30	27, 29	e1a 37006	. . . . . . . . . 10 $/\$ $\/$ $/\$
31	30	in1 36941	. . . . . . . . 9 $/\$ $\/$ $/\$
32		idn1 36944	. . . . . . . . . . . 12 $/\$ $/\$
33		simpl 459	. . . . . . . . . . . 12 $/\$
34	32, 33	e1a 37006	. . . . . . . . . . 11 $/\$
35		orc 387	. . . . . . . . . . 11 $\/$ $/\$
36	34, 35	e1a 37006	. . . . . . . . . 10 $/\$ $\/$ $/\$
37	36	in1 36941	. . . . . . . . 9 $/\$ $\/$ $/\$
38	31, 37	jaoi 381	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$ $/\$
39		olc 386	. . . . . . . . . . 11 $/\$ $\/$ $/\$
40	13, 39	e1a 37006	. . . . . . . . . 10 $/\$ $\/$ $/\$
41	40	in1 36941	. . . . . . . . 9 $/\$ $\/$ $/\$
42		idn1 36944	. . . . . . . . . . . 12 $/\$ $/\$
43		simpr 463	. . . . . . . . . . . 12 $/\$
44	42, 43	e1a 37006	. . . . . . . . . . 11 $/\$
45	44, 35	e1a 37006	. . . . . . . . . 10 $/\$ $\/$ $/\$
46	45	in1 36941	. . . . . . . . 9 $/\$ $\/$ $/\$
47	41, 46	jaoi 381	. . . . . . . 8 $/\$ $\/$ $/\$ $\/$ $/\$
48	38, 47	jaoi 381	. . . . . . 7 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
49	26, 48	sylbir 217	. . . . . 6 $\/$ $/\$ $\/$ $\/$ $/\$
50	24, 49	impbii 191	. . . . 5 $\/$ $/\$ $\/$ $/\$ $\/$
51	4, 50	bitri 253	. . . 4 $\$ $\/$ $/\$ $\/$
52		eldif 3414	. . . . 5 $\$ $\$ $/\$ $\$
53		elun 3574	. . . . . 6 $\/$
54		eldif 3414	. . . . . . . 8 $\$ $/\$
55	54	notbii 298	. . . . . . 7 $\$ $/\$
56		pm4.53 495	. . . . . . 7 $/\$ $\/$
57	55, 56	bitri 253	. . . . . 6 $\$ $\/$
58	53, 57	anbi12i 703	. . . . 5 $/\$ $\$ $\/$ $/\$ $\/$
59	52, 58	bitri 253	. . . 4 $\$ $\$ $\/$ $/\$ $\/$
60	51, 59	bitr4i 256	. . 3 $\$ $\$ $\$
61	60	ax-gen 1669	. 2 $\$ $\$ $\$
62		dfcleq 2445	. . 3 $\$ $\$ $\$ $\$ $\$ $\$
63	62	biimpri 210	. 2 $\$ $\$ $\$ $\$ $\$ $\$
64	61, 63	e0a 37159	1 $\$ $\$ $\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 188 $\/$ wo 370 $/\$ wa 371

wal 1442

wceq 1444

wcel 1887 $\$ cdif 3401

cun 3402

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-v 3047 df-dif 3407 df-un 3409 df-vd1 36940

This theorem is referenced by: (None)

W3C validator