Users' Mathboxes 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::  |-  ( 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 3574 . . . . . 6  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  x  e.  ( B  \  C
) ) )
2 eldif 3414 . . . . . . 7  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
32orbi2i 522 . . . . . 6  |-  ( ( x  e.  A  \/  x  e.  ( B  \  C ) )  <->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
41, 3bitri 253 . . . . 5  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C )
) )
5 idn1 36944 . . . . . . . . . 10  |-  (. x  e.  A  ->.  x  e.  A ).
6 orc 387 . . . . . . . . . 10  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
75, 6e1a 37006 . . . . . . . . 9  |-  (. x  e.  A  ->.  ( x  e.  A  \/  x  e.  B ) ).
8 olc 386 . . . . . . . . . 10  |-  ( x  e.  A  ->  ( -.  x  e.  C  \/  x  e.  A
) )
95, 8e1a 37006 . . . . . . . . 9  |-  (. x  e.  A  ->.  ( -.  x  e.  C  \/  x  e.  A ) ).
10 pm3.2 449 . . . . . . . . 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 37067 . . . . . . . 8  |-  (. x  e.  A  ->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
1211in1 36941 . . . . . . 7  |-  ( x  e.  A  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) )
13 idn1 36944 . . . . . . . . . . 11  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  B  /\  -.  x  e.  C
) ).
14 simpl 459 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  x  e.  B )
1513, 14e1a 37006 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  x  e.  B ).
16 olc 386 . . . . . . . . . 10  |-  ( x  e.  B  ->  (
x  e.  A  \/  x  e.  B )
)
1715, 16e1a 37006 . . . . . . . . 9  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  x  e.  B
) ).
18 simpr 463 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  -.  x  e.  C )
1913, 18e1a 37006 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  -.  x  e.  C ).
20 orc 387 . . . . . . . . . 10  |-  ( -.  x  e.  C  -> 
( -.  x  e.  C  \/  x  e.  A ) )
2119, 20e1a 37006 . . . . . . . . 9  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( -.  x  e.  C  \/  x  e.  A ) ).
2217, 21, 10e11 37067 . . . . . . . 8  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
2322in1 36941 . . . . . . 7  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
2412, 23jaoi 381 . . . . . 6  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) )  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) )
25 anddi 881 . . . . . . . 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 206 . . . . . . 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 36944 . . . . . . . . . . 11  |-  (. (
x  e.  A  /\  -.  x  e.  C
) 
->.  ( x  e.  A  /\  -.  x  e.  C
) ).
28 simpl 459 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  x  e.  A )
2928orcd 394 . . . . . . . . . . 11  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
3027, 29e1a 37006 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3130in1 36941 . . . . . . . . 9  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
32 idn1 36944 . . . . . . . . . . . 12  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  /\  x  e.  A ) ).
33 simpl 459 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  x  e.  A )  ->  x  e.  A )
3432, 33e1a 37006 . . . . . . . . . . 11  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  x  e.  A ).
35 orc 387 . . . . . . . . . . 11  |-  ( x  e.  A  ->  (
x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
3634, 35e1a 37006 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3736in1 36941 . . . . . . . . 9  |-  ( ( x  e.  A  /\  x  e.  A )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
3831, 37jaoi 381 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  -.  x  e.  C
)  \/  ( x  e.  A  /\  x  e.  A ) )  -> 
( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
39 olc 386 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
4013, 39e1a 37006 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4140in1 36941 . . . . . . . . 9  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
42 idn1 36944 . . . . . . . . . . . 12  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  ( x  e.  B  /\  x  e.  A ) ).
43 simpr 463 . . . . . . . . . . . 12  |-  ( ( x  e.  B  /\  x  e.  A )  ->  x  e.  A )
4442, 43e1a 37006 . . . . . . . . . . 11  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  x  e.  A ).
4544, 35e1a 37006 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4645in1 36941 . . . . . . . . 9  |-  ( ( x  e.  B  /\  x  e.  A )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
4741, 46jaoi 381 . . . . . . . 8  |-  ( ( ( x  e.  B  /\  -.  x  e.  C
)  \/  ( x  e.  B  /\  x  e.  A ) )  -> 
( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
4838, 47jaoi 381 . . . . . . 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 217 . . . . . 6  |-  ( ( ( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
5024, 49impbii 191 . . . . 5  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) )  <->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
514, 50bitri 253 . . . 4  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) )
52 eldif 3414 . . . . 5  |-  ( x  e.  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  ( x  e.  ( A  u.  B
)  /\  -.  x  e.  ( C  \  A
) ) )
53 elun 3574 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
54 eldif 3414 . . . . . . . 8  |-  ( x  e.  ( C  \  A )  <->  ( x  e.  C  /\  -.  x  e.  A ) )
5554notbii 298 . . . . . . 7  |-  ( -.  x  e.  ( C 
\  A )  <->  -.  (
x  e.  C  /\  -.  x  e.  A
) )
56 pm4.53 495 . . . . . . 7  |-  ( -.  ( x  e.  C  /\  -.  x  e.  A
)  <->  ( -.  x  e.  C  \/  x  e.  A ) )
5755, 56bitri 253 . . . . . 6  |-  ( -.  x  e.  ( C 
\  A )  <->  ( -.  x  e.  C  \/  x  e.  A )
)
5853, 57anbi12i 703 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  /\  -.  x  e.  ( C  \  A ) )  <-> 
( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) )
5952, 58bitri 253 . . . 4  |-  ( x  e.  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
6051, 59bitr4i 256 . . 3  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  x  e.  (
( A  u.  B
)  \  ( C  \  A ) ) )
6160ax-gen 1669 . 2  |-  A. x
( x  e.  ( A  u.  ( B 
\  C ) )  <-> 
x  e.  ( ( A  u.  B ) 
\  ( C  \  A ) ) )
62 dfcleq 2445 . . 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 210 . 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 37159 1  |-  ( A  u.  ( B  \  C ) )  =  ( ( A  u.  B )  \  ( C  \  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188    \/ wo 370    /\ wa 371   A.wal 1442    = wceq 1444    e. wcel 1887    \ cdif 3401    u. 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)
  Copyright terms: Public domain W3C validator