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

Theorem undif3VD 28974
Description: The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3442. 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 3442 is undif3VD 28974 without virtual deductions and was automatically derived from undif3VD 28974.
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 3329 . . . . . 6  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  x  e.  ( B  \  C
) ) )
2 eldif 3175 . . . . . . 7  |-  ( x  e.  ( B  \  C )  <->  ( x  e.  B  /\  -.  x  e.  C ) )
32orbi2i 505 . . . . . 6  |-  ( ( x  e.  A  \/  x  e.  ( B  \  C ) )  <->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
41, 3bitri 240 . . . . 5  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C )
) )
5 idn1 28641 . . . . . . . . . 10  |-  (. x  e.  A  ->.  x  e.  A ).
6 orc 374 . . . . . . . . . 10  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
75, 6e1_ 28704 . . . . . . . . 9  |-  (. x  e.  A  ->.  ( x  e.  A  \/  x  e.  B ) ).
8 olc 373 . . . . . . . . . 10  |-  ( x  e.  A  ->  ( -.  x  e.  C  \/  x  e.  A
) )
95, 8e1_ 28704 . . . . . . . . 9  |-  (. x  e.  A  ->.  ( -.  x  e.  C  \/  x  e.  A ) ).
10 pm3.2 434 . . . . . . . . 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 28765 . . . . . . . 8  |-  (. x  e.  A  ->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
1211in1 28638 . . . . . . 7  |-  ( x  e.  A  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) )
13 idn1 28641 . . . . . . . . . . 11  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  B  /\  -.  x  e.  C
) ).
14 simpl 443 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  x  e.  B )
1513, 14e1_ 28704 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  x  e.  B ).
16 olc 373 . . . . . . . . . 10  |-  ( x  e.  B  ->  (
x  e.  A  \/  x  e.  B )
)
1715, 16e1_ 28704 . . . . . . . . 9  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  x  e.  B
) ).
18 simpr 447 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  -.  x  e.  C )
1913, 18e1_ 28704 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  -.  x  e.  C ).
20 orc 374 . . . . . . . . . 10  |-  ( -.  x  e.  C  -> 
( -.  x  e.  C  \/  x  e.  A ) )
2119, 20e1_ 28704 . . . . . . . . 9  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( -.  x  e.  C  \/  x  e.  A ) ).
2217, 21, 10e11 28765 . . . . . . . 8  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
2322in1 28638 . . . . . . 7  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
2412, 23jaoi 368 . . . . . 6  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) )  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) )
25 anddi 840 . . . . . . . 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 193 . . . . . . 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 28641 . . . . . . . . . . 11  |-  (. (
x  e.  A  /\  -.  x  e.  C
) 
->.  ( x  e.  A  /\  -.  x  e.  C
) ).
28 simpl 443 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  x  e.  A )
2928orcd 381 . . . . . . . . . . 11  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
3027, 29e1_ 28704 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3130in1 28638 . . . . . . . . 9  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
32 idn1 28641 . . . . . . . . . . . 12  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  /\  x  e.  A ) ).
33 simpl 443 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  x  e.  A )  ->  x  e.  A )
3432, 33e1_ 28704 . . . . . . . . . . 11  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  x  e.  A ).
35 orc 374 . . . . . . . . . . 11  |-  ( x  e.  A  ->  (
x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
3634, 35e1_ 28704 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3736in1 28638 . . . . . . . . 9  |-  ( ( x  e.  A  /\  x  e.  A )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
3831, 37jaoi 368 . . . . . . . 8  |-  ( ( ( x  e.  A  /\  -.  x  e.  C
)  \/  ( x  e.  A  /\  x  e.  A ) )  -> 
( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
39 olc 373 . . . . . . . . . . 11  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
4013, 39e1_ 28704 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4140in1 28638 . . . . . . . . 9  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
42 idn1 28641 . . . . . . . . . . . 12  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  ( x  e.  B  /\  x  e.  A ) ).
43 simpr 447 . . . . . . . . . . . 12  |-  ( ( x  e.  B  /\  x  e.  A )  ->  x  e.  A )
4442, 43e1_ 28704 . . . . . . . . . . 11  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  x  e.  A ).
4544, 35e1_ 28704 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4645in1 28638 . . . . . . . . 9  |-  ( ( x  e.  B  /\  x  e.  A )  ->  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
4741, 46jaoi 368 . . . . . . . 8  |-  ( ( ( x  e.  B  /\  -.  x  e.  C
)  \/  ( x  e.  B  /\  x  e.  A ) )  -> 
( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) )
4838, 47jaoi 368 . . . . . . 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 204 . . . . . 6  |-  ( ( ( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
5024, 49impbii 180 . . . . 5  |-  ( ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) )  <->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
514, 50bitri 240 . . . 4  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) )
52 eldif 3175 . . . . 5  |-  ( x  e.  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  ( x  e.  ( A  u.  B
)  /\  -.  x  e.  ( C  \  A
) ) )
53 elun 3329 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
54 eldif 3175 . . . . . . . 8  |-  ( x  e.  ( C  \  A )  <->  ( x  e.  C  /\  -.  x  e.  A ) )
5554notbii 287 . . . . . . 7  |-  ( -.  x  e.  ( C 
\  A )  <->  -.  (
x  e.  C  /\  -.  x  e.  A
) )
56 pm4.53 478 . . . . . . 7  |-  ( -.  ( x  e.  C  /\  -.  x  e.  A
)  <->  ( -.  x  e.  C  \/  x  e.  A ) )
5755, 56bitri 240 . . . . . 6  |-  ( -.  x  e.  ( C 
\  A )  <->  ( -.  x  e.  C  \/  x  e.  A )
)
5853, 57anbi12i 678 . . . . 5  |-  ( ( x  e.  ( A  u.  B )  /\  -.  x  e.  ( C  \  A ) )  <-> 
( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) )
5952, 58bitri 240 . . . 4  |-  ( x  e.  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  ( (
x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A ) ) )
6051, 59bitr4i 243 . . 3  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  x  e.  (
( A  u.  B
)  \  ( C  \  A ) ) )
6160ax-gen 1536 . 2  |-  A. x
( x  e.  ( A  u.  ( B 
\  C ) )  <-> 
x  e.  ( ( A  u.  B ) 
\  ( C  \  A ) ) )
62 dfcleq 2290 . . 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 197 . 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_ 28861 1  |-  ( A  u.  ( B  \  C ) )  =  ( ( A  u.  B )  \  ( C  \  A ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176    \/ wo 357    /\ wa 358   A.wal 1530    = wceq 1632    e. wcel 1696    \ cdif 3162    u. cun 3163
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-dif 3168  df-un 3170  df-vd1 28637
  Copyright terms: Public domain W3C validator