Users' Mathboxes 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::  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  x  e.  ( B  \  C ) ) )
2::  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
3:2:  |-  ( ( x  e.  A  \/  x  e.  ( B  \  C ) )  <->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
4:1,3:  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
5::  |-  (. x  e.  A  ->.  x  e.  A ).
6:5:  |-  (. x  e.  A  ->.  ( x  e.  A  \/  x  e.  B ) ).
7:5:  |-  (. x  e.  A  ->.  ( -.  x  e.  C  \/  x  e.  A ) ).
8:6,7:  |-  (. x  e.  A  ->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) ).
9:8:  |-  ( x  e.  A  ->  ( ( x  e.  A  \/  x  e.  B )  /\  (  -.  x  e.  C  \/  x  e.  A ) ) )
10::  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( x  e.  B  /\  -.  x  e.  C ) ).
11:10:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  x  e.  B ).
12:10:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  -.  x  e.  C  ).
13:11:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( x  e.  A  \/  x  e.  B ) ).
14:12:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( -.  x  e.  C  \/  x  e.  A ) ).
15:13,14:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) ).
16:15:  |-  ( ( x  e.  B  /\  -.  x  e.  C )  ->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
17:9,16:  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) )  ->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
18::  |-  (. ( x  e.  A  /\  -.  x  e.  C )  ->.  ( x  e.  A  /\  -.  x  e.  C ) ).
19:18:  |-  (. ( x  e.  A  /\  -.  x  e.  C )  ->.  x  e.  A ).
20:18:  |-  (. ( x  e.  A  /\  -.  x  e.  C )  ->.  -.  x  e.  C  ).
21:18:  |-  (. ( x  e.  A  /\  -.  x  e.  C )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) ).
22:21:  |-  ( ( x  e.  A  /\  -.  x  e.  C )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
23::  |-  (. ( x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  /\  x  e.  A ) ).
24:23:  |-  (. ( x  e.  A  /\  x  e.  A )  ->.  x  e.  A ).
25:24:  |-  (. ( x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) ).
26:25:  |-  ( ( x  e.  A  /\  x  e.  A )  ->  ( x  e.  A  \/  (  x  e.  B  /\  -.  x  e.  C ) ) )
27:10:  |-  (. ( x  e.  B  /\  -.  x  e.  C )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) ).
28:27:  |-  ( ( x  e.  B  /\  -.  x  e.  C )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
29::  |-  (. ( x  e.  B  /\  x  e.  A )  ->.  ( x  e.  B  /\  x  e.  A ) ).
30:29:  |-  (. ( x  e.  B  /\  x  e.  A )  ->.  x  e.  A ).
31:30:  |-  (. ( x  e.  B  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) ).
32:31:  |-  ( ( x  e.  B  /\  x  e.  A )  ->  ( x  e.  A  \/  (  x  e.  B  /\  -.  x  e.  C ) ) )
33:22,26:  |-  ( ( ( x  e.  A  /\  -.  x  e.  C )  \/  ( x  e.  A  /\  x  e.  A ) )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
34:28,32:  |-  ( ( ( x  e.  B  /\  -.  x  e.  C )  \/  ( x  e.  B  /\  x  e.  A ) )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
35:33,34:  |-  ( ( ( ( x  e.  A  /\  -.  x  e.  C )  \/  ( x  e.  A  /\  x  e.  A ) )  \/  ( ( x  e.  B  /\  -.  x  e.  C )  \/  ( x  e.  B  /\  x  e.  A ) ) )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
36::  |-  ( ( ( ( x  e.  A  /\  -.  x  e.  C )  \/  ( x  e.  A  /\  x  e.  A ) )  \/  ( ( x  e.  B  /\  -.  x  e.  C )  \/  ( x  e.  B  /\  x  e.  A ) ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
37:36,35:  |-  ( ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) ) )
38:17,37:  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
39::  |-  ( x  e.  ( C  \  A )  <->  ( x  e.  C  /\  -.  x  e.  A ) )
40:39:  |-  ( -.  x  e.  ( C  \  A )  <->  -.  ( x  e.  C  /\  -.  x  e.  A ) )
41::  |-  ( -.  ( x  e.  C  /\  -.  x  e.  A )  <->  ( -.  x  e.  C  \/  x  e.  A ) )
42:40,41:  |-  ( -.  x  e.  ( C  \  A )  <->  ( -.  x  e.  C  \/  x  e.  A ) )
43::  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B  ) )
44:43,42:  |-  ( ( x  e.  ( A  u.  B )  /\  -.  x  e.  ( C  \  A )  )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  /\  x  e.  A ) ) )
45::  |-  ( x  e.  ( ( A  u.  B )  \  ( C  \  A ) )  <->  (  x  e.  ( A  u.  B )  /\  -.  x  e.  ( C  \  A ) ) )
46:45,44:  |-  ( x  e.  ( ( A  u.  B )  \  ( C  \  A ) )  <->  (  ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
47:4,38:  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
48:46,47:  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  x  e.  ( ( A  u.  B )  \  ( C  \  A ) ) )
49:48:  |-  A. x ( x  e.  ( A  u.  ( B  \  C ) )  <->  x  e.  ( ( A  u.  B )  \  ( C  \  A ) ) )
qed:49:  |-  ( A  u.  ( B  \  C ) )  =  ( ( A  u.  B )  \  ( C  \  A ) )
(Contributed by Alan Sare, 17-Apr-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
undif3VD  |-  ( A  u.  ( B  \  C ) )  =  ( ( A  u.  B )  \  ( C  \  A ) )

Proof of Theorem undif3VD
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 elun 3640 . . . . . 6  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  x  e.  ( B  \  C
) ) )
2 eldif 3481 . . . . . . 7  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
32orbi2i 519 . . . . . 6  |-  ( ( x  e.  A  \/  x  e.  ( B  \  C ) )  <->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
41, 3bitri 249 . . . . 5  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C )
) )
5 idn1 32308 . . . . . . . . . 10  |-  (. x  e.  A  ->.  x  e.  A ).
6 orc 385 . . . . . . . . . 10  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
75, 6e1a 32370 . . . . . . . . 9  |-  (. x  e.  A  ->.  ( x  e.  A  \/  x  e.  B ) ).
8 olc 384 . . . . . . . . . 10  |-  ( x  e.  A  ->  ( -.  x  e.  C  \/  x  e.  A
) )
95, 8e1a 32370 . . . . . . . . 9  |-  (. x  e.  A  ->.  ( -.  x  e.  C  \/  x  e.  A ) ).
10 pm3.2 447 . . . . . . . . 9  |-  ( ( x  e.  A  \/  x  e.  B )  ->  ( ( -.  x  e.  C  \/  x  e.  A )  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) ) )
117, 9, 10e11 32431 . . . . . . . 8  |-  (. x  e.  A  ->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
1211in1 32305 . . . . . . 7  |-  ( x  e.  A  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) )
13 idn1 32308 . . . . . . . . . . 11  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  B  /\  -.  x  e.  C
) ).
14 simpl 457 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  x  e.  B )
1513, 14e1a 32370 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  x  e.  B ).
16 olc 384 . . . . . . . . . 10  |-  ( x  e.  B  ->  (
x  e.  A  \/  x  e.  B )
)
1715, 16e1a 32370 . . . . . . . . 9  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  x  e.  B
) ).
18 simpr 461 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  -.  x  e.  C )
1913, 18e1a 32370 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  -.  x  e.  C ).
20 orc 385 . . . . . . . . . 10  |-  ( -.  x  e.  C  -> 
( -.  x  e.  C  \/  x  e.  A ) )
2119, 20e1a 32370 . . . . . . . . 9  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( -.  x  e.  C  \/  x  e.  A ) ).
2217, 21, 10e11 32431 . . . . . . . 8  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
2322in1 32305 . . . . . . 7  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
2412, 23jaoi 379 . . . . . 6  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) )  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) )
25 anddi 866 . . . . . . . 8  |-  ( ( ( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
)  <->  ( ( ( x  e.  A  /\  -.  x  e.  C
)  \/  ( x  e.  A  /\  x  e.  A ) )  \/  ( ( x  e.  B  /\  -.  x  e.  C )  \/  (
x  e.  B  /\  x  e.  A )
) ) )
2625bicomi 202 . . . . . . 7  |-  ( ( ( ( x  e.  A  /\  -.  x  e.  C )  \/  (
x  e.  A  /\  x  e.  A )
)  \/  ( ( x  e.  B  /\  -.  x  e.  C
)  \/  ( x  e.  B  /\  x  e.  A ) ) )  <-> 
( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) )
27 idn1 32308 . . . . . . . . . . 11  |-  (. (
x  e.  A  /\  -.  x  e.  C
) 
->.  ( x  e.  A  /\  -.  x  e.  C
) ).
28 simpl 457 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  x  e.  A )
2928orcd 392 . . . . . . . . . . 11  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
3027, 29e1a 32370 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3130in1 32305 . . . . . . . . 9  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
32 idn1 32308 . . . . . . . . . . . 12  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  /\  x  e.  A ) ).
33 simpl 457 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  x  e.  A )  ->  x  e.  A )
3432, 33e1a 32370 . . . . . . . . . . 11  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  x  e.  A ).
35 orc 385 . . . . . . . . . . 11  |-  ( x  e.  A  ->  (
x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
3634, 35e1a 32370 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3736in1 32305 . . . . . . . . 9  |-  ( ( x  e.  A  /\  x  e.  A )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
3831, 37jaoi 379 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  -.  x  e.  C
)  \/  ( x  e.  A  /\  x  e.  A ) )  -> 
( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
39 olc 384 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
4013, 39e1a 32370 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4140in1 32305 . . . . . . . . 9  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
42 idn1 32308 . . . . . . . . . . . 12  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  ( x  e.  B  /\  x  e.  A ) ).
43 simpr 461 . . . . . . . . . . . 12  |-  ( ( x  e.  B  /\  x  e.  A )  ->  x  e.  A )
4442, 43e1a 32370 . . . . . . . . . . 11  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  x  e.  A ).
4544, 35e1a 32370 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4645in1 32305 . . . . . . . . 9  |-  ( ( x  e.  B  /\  x  e.  A )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
4741, 46jaoi 379 . . . . . . . 8  |-  ( ( ( x  e.  B  /\  -.  x  e.  C
)  \/  ( x  e.  B  /\  x  e.  A ) )  -> 
( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
4838, 47jaoi 379 . . . . . . 7  |-  ( ( ( ( x  e.  A  /\  -.  x  e.  C )  \/  (
x  e.  A  /\  x  e.  A )
)  \/  ( ( x  e.  B  /\  -.  x  e.  C
)  \/  ( x  e.  B  /\  x  e.  A ) ) )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C )
) )
4926, 48sylbir 213 . . . . . 6  |-  ( ( ( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
5024, 49impbii 188 . . . . 5  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) )  <->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
514, 50bitri 249 . . . 4  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) )
52 eldif 3481 . . . . 5  |-  ( x  e.  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  ( x  e.  ( A  u.  B
)  /\  -.  x  e.  ( C  \  A
) ) )
53 elun 3640 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
54 eldif 3481 . . . . . . . 8  |-  ( x  e.  ( C  \  A )  <->  ( x  e.  C  /\  -.  x  e.  A ) )
5554notbii 296 . . . . . . 7  |-  ( -.  x  e.  ( C 
\  A )  <->  -.  (
x  e.  C  /\  -.  x  e.  A
) )
56 pm4.53 492 . . . . . . 7  |-  ( -.  ( x  e.  C  /\  -.  x  e.  A
)  <->  ( -.  x  e.  C  \/  x  e.  A ) )
5755, 56bitri 249 . . . . . 6  |-  ( -.  x  e.  ( C 
\  A )  <->  ( -.  x  e.  C  \/  x  e.  A )
)
5853, 57anbi12i 697 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  /\  -.  x  e.  ( C  \  A ) )  <-> 
( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) )
5952, 58bitri 249 . . . 4  |-  ( x  e.  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
6051, 59bitr4i 252 . . 3  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  x  e.  (
( A  u.  B
)  \  ( C  \  A ) ) )
6160ax-gen 1596 . 2  |-  A. x
( x  e.  ( A  u.  ( B 
\  C ) )  <-> 
x  e.  ( ( A  u.  B ) 
\  ( C  \  A ) ) )
62 dfcleq 2455 . . 3  |-  ( ( A  u.  ( B 
\  C ) )  =  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  A. x
( x  e.  ( A  u.  ( B 
\  C ) )  <-> 
x  e.  ( ( A  u.  B ) 
\  ( C  \  A ) ) ) )
6362biimpri 206 . 2  |-  ( A. x ( x  e.  ( A  u.  ( B  \  C ) )  <-> 
x  e.  ( ( A  u.  B ) 
\  ( C  \  A ) ) )  ->  ( A  u.  ( B  \  C ) )  =  ( ( A  u.  B ) 
\  ( C  \  A ) ) )
6461, 63e0a 32526 1  |-  ( A  u.  ( B  \  C ) )  =  ( ( A  u.  B )  \  ( C  \  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184    \/ wo 368    /\ wa 369   A.wal 1372    = wceq 1374    e. wcel 1762    \ cdif 3468    u. 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)
  Copyright terms: Public domain W3C validator