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

Theorem undif3VD 33415
Description: The first equality of Exercise 13 of [TakeutiZaring] p. 22. Virtual deduction proof of undif3 3744. 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 3744 is undif3VD 33415 without virtual deductions and was automatically derived from undif3VD 33415.
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 3630 . . . . . 6  |-  ( x  e.  ( A  u.  ( B  \  C ) )  <->  ( x  e.  A  \/  x  e.  ( B  \  C
) ) )
2 eldif 3471 . . . . . . 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 33084 . . . . . . . . . 10  |-  (. x  e.  A  ->.  x  e.  A ).
6 orc 385 . . . . . . . . . 10  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
75, 6e1a 33146 . . . . . . . . 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 33146 . . . . . . . . 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 33207 . . . . . . . 8  |-  (. x  e.  A  ->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
1211in1 33081 . . . . . . 7  |-  ( x  e.  A  ->  (
( x  e.  A  \/  x  e.  B
)  /\  ( -.  x  e.  C  \/  x  e.  A )
) )
13 idn1 33084 . . . . . . . . . . 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 33146 . . . . . . . . . 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 33146 . . . . . . . . 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 33146 . . . . . . . . . 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 33146 . . . . . . . . 9  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( -.  x  e.  C  \/  x  e.  A ) ).
2217, 21, 10e11 33207 . . . . . . . 8  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( ( x  e.  A  \/  x  e.  B )  /\  ( -.  x  e.  C  \/  x  e.  A
) ) ).
2322in1 33081 . . . . . . 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 870 . . . . . . . 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 33084 . . . . . . . . . . 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 33146 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3130in1 33081 . . . . . . . . 9  |-  ( ( x  e.  A  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
32 idn1 33084 . . . . . . . . . . . 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 33146 . . . . . . . . . . 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 33146 . . . . . . . . . 10  |-  (. (
x  e.  A  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
3736in1 33081 . . . . . . . . 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 33146 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  -.  x  e.  C
) 
->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4140in1 33081 . . . . . . . . 9  |-  ( ( x  e.  B  /\  -.  x  e.  C
)  ->  ( x  e.  A  \/  (
x  e.  B  /\  -.  x  e.  C
) ) )
42 idn1 33084 . . . . . . . . . . . 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 33146 . . . . . . . . . . 11  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  x  e.  A ).
4544, 35e1a 33146 . . . . . . . . . 10  |-  (. (
x  e.  B  /\  x  e.  A )  ->.  ( x  e.  A  \/  ( x  e.  B  /\  -.  x  e.  C
) ) ).
4645in1 33081 . . . . . . . . 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 3471 . . . . 5  |-  ( x  e.  ( ( A  u.  B )  \ 
( C  \  A
) )  <->  ( x  e.  ( A  u.  B
)  /\  -.  x  e.  ( C  \  A
) ) )
53 elun 3630 . . . . . 6  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
54 eldif 3471 . . . . . . . 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 1605 . 2  |-  A. x
( x  e.  ( A  u.  ( B 
\  C ) )  <-> 
x  e.  ( ( A  u.  B ) 
\  ( C  \  A ) ) )
62 dfcleq 2436 . . 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 33302 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 1381    = wceq 1383    e. wcel 1804    \ cdif 3458    u. cun 3459
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-dif 3464  df-un 3466  df-vd1 33080
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator