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

Theorem undif3VD 28848
Description: The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3594. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. undif3 3594 is undif3VD 28848 without virtual deductions and was automatically derived from undif3VD 28848.
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 3480 . . . . . 6  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  x  e.  ( B  \  C
) ) )
2 eldif 3322 . . . . . . 7  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
32orbi2i 506 . . . . . 6  |-  ( ( x  e.  A  \/  x  e.  ( B  \  C ) )  <->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
41, 3bitri 241 . . . . 5  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C )
) )
5 idn1 28519 . . . . . . . . . 10  |-  (. x  e.  A  ->.  x  e.  A ).
6 orc 375 . . . . . . . . . 10  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
75, 6e1_ 28582 . . . . . . . . 9  |-  (. x  e.  A  ->.  ( x  e.  A  \/  x  e.  B ) ).
8 olc 374 . . . . . . . . . 10  |-  ( x  e.  A  ->  ( -.  x  e.  C  \/  x  e.  A
) )
95, 8e1_ 28582 . . . . . . . . 9  |-  (. x  e.  A  ->.  ( -.  x  e.  C  \/  x  e.  A ) ).
10 pm3.2 435 . . . . . . . . 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 28643 . . . . . . . 8  |-  (. x  e.  A  ->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
1211in1 28516 . . . . . . 7  |-  ( x  e.  A  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) )
13 idn1 28519 . . . . . . . . . . 11  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  B  /\  -.  x  e.  C
) ).
14 simpl 444 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  x  e.  B )
1513, 14e1_ 28582 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  x  e.  B ).
16 olc 374 . . . . . . . . . 10  |-  ( x  e.  B  ->  (
x  e.  A  \/  x  e.  B )
)
1715, 16e1_ 28582 . . . . . . . . 9  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  x  e.  B
) ).
18 simpr 448 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  -.  x  e.  C )
1913, 18e1_ 28582 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  -.  x  e.  C ).
20 orc 375 . . . . . . . . . 10  |-  ( -.  x  e.  C  -> 
( -.  x  e.  C  \/  x  e.  A ) )
2119, 20e1_ 28582 . . . . . . . . 9  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( -.  x  e.  C  \/  x  e.  A ) ).
2217, 21, 10e11 28643 . . . . . . . 8  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
2322in1 28516 . . . . . . 7  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
2412, 23jaoi 369 . . . . . 6  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) )  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) )
25 anddi 841 . . . . . . . 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 194 . . . . . . 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 28519 . . . . . . . . . . 11  |-  (. (
x  e.  A  /\  -.  x  e.  C
) 
->.  ( x  e.  A  /\  -.  x  e.  C
) ).
28 simpl 444 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  x  e.  A )
2928orcd 382 . . . . . . . . . . 11  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
3027, 29e1_ 28582 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3130in1 28516 . . . . . . . . 9  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
32 idn1 28519 . . . . . . . . . . . 12  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  /\  x  e.  A ) ).
33 simpl 444 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  x  e.  A )  ->  x  e.  A )
3432, 33e1_ 28582 . . . . . . . . . . 11  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  x  e.  A ).
35 orc 375 . . . . . . . . . . 11  |-  ( x  e.  A  ->  (
x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
3634, 35e1_ 28582 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3736in1 28516 . . . . . . . . 9  |-  ( ( x  e.  A  /\  x  e.  A )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
3831, 37jaoi 369 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  -.  x  e.  C
)  \/  ( x  e.  A  /\  x  e.  A ) )  -> 
( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
39 olc 374 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
4013, 39e1_ 28582 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4140in1 28516 . . . . . . . . 9  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
42 idn1 28519 . . . . . . . . . . . 12  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  ( x  e.  B  /\  x  e.  A ) ).
43 simpr 448 . . . . . . . . . . . 12  |-  ( ( x  e.  B  /\  x  e.  A )  ->  x  e.  A )
4442, 43e1_ 28582 . . . . . . . . . . 11  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  x  e.  A ).
4544, 35e1_ 28582 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4645in1 28516 . . . . . . . . 9  |-  ( ( x  e.  B  /\  x  e.  A )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
4741, 46jaoi 369 . . . . . . . 8  |-  ( ( ( x  e.  B  /\  -.  x  e.  C
)  \/  ( x  e.  B  /\  x  e.  A ) )  -> 
( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
4838, 47jaoi 369 . . . . . . 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 205 . . . . . 6  |-  ( ( ( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
5024, 49impbii 181 . . . . 5  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) )  <->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
514, 50bitri 241 . . . 4  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) )
52 eldif 3322 . . . . 5  |-  ( x  e.  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  ( x  e.  ( A  u.  B
)  /\  -.  x  e.  ( C  \  A
) ) )
53 elun 3480 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
54 eldif 3322 . . . . . . . 8  |-  ( x  e.  ( C  \  A )  <->  ( x  e.  C  /\  -.  x  e.  A ) )
5554notbii 288 . . . . . . 7  |-  ( -.  x  e.  ( C 
\  A )  <->  -.  (
x  e.  C  /\  -.  x  e.  A
) )
56 pm4.53 479 . . . . . . 7  |-  ( -.  ( x  e.  C  /\  -.  x  e.  A
)  <->  ( -.  x  e.  C  \/  x  e.  A ) )
5755, 56bitri 241 . . . . . 6  |-  ( -.  x  e.  ( C 
\  A )  <->  ( -.  x  e.  C  \/  x  e.  A )
)
5853, 57anbi12i 679 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  /\  -.  x  e.  ( C  \  A ) )  <-> 
( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) )
5952, 58bitri 241 . . . 4  |-  ( x  e.  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
6051, 59bitr4i 244 . . 3  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  x  e.  (
( A  u.  B
)  \  ( C  \  A ) ) )
6160ax-gen 1555 . 2  |-  A. x
( x  e.  ( A  u.  ( B 
\  C ) )  <-> 
x  e.  ( ( A  u.  B ) 
\  ( C  \  A ) ) )
62 dfcleq 2429 . . 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 198 . 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, 63e0_ 28738 1  |-  ( A  u.  ( B  \  C ) )  =  ( ( A  u.  B )  \  ( C  \  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    \/ wo 358    /\ wa 359   A.wal 1549    = wceq 1652    e. wcel 1725    \ cdif 3309    u. cun 3310
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-dif 3315  df-un 3317  df-vd1 28515
  Copyright terms: Public domain W3C validator