undif3VD

Description: The first equality of Exercise 13 of TakeutiZaring p. 22. Virtual deduction proof of undif3 . 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 is undif3VD without virtual deductions and was automatically derived from undif3VD .

		Ref	Expression
	Assertion	undif3VD	$⊢ A \cup (B ∖ C) = (A \cup B) ∖ (C ∖ A)$

Proof

Step	Hyp	Ref	Expression
1		elun	$⊢ x \in (A \cup (B ∖ C)) \leftrightarrow (x \in A \lor x \in (B ∖ C))$
2		eldif	$⊢ x \in (B ∖ C) \leftrightarrow (x \in B \land \neg x \in C)$
3	2	orbi2i	$⊢ (x \in A \lor x \in (B ∖ C)) \leftrightarrow (x \in A \lor (x \in B \land \neg x \in C))$
4	1 3	bitri	$⊢ x \in (A \cup (B ∖ C)) \leftrightarrow (x \in A \lor (x \in B \land \neg x \in C))$
5		idn1	$⊢ (x \in A \to x \in A)$
6		orc	$⊢ x \in A \to (x \in A \lor x \in B)$
7	5 6	e1a	$⊢ (x \in A \to (x \in A \lor x \in B))$
8		olc	$⊢ x \in A \to (\neg x \in C \lor x \in A)$
9	5 8	e1a	$⊢ (x \in A \to (\neg x \in C \lor x \in A))$
10		pm3.2	$⊢ (x \in A \lor x \in B) \to ((\neg x \in C \lor x \in A) \to ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A)))$
11	7 9 10	e11	$⊢ (x \in A \to ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A)))$
12	11	in1	$⊢ x \in A \to ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
13		idn1	$⊢ ((x \in B \land \neg x \in C) \to (x \in B \land \neg x \in C))$
14		simpl	$⊢ (x \in B \land \neg x \in C) \to x \in B$
15	13 14	e1a	$⊢ ((x \in B \land \neg x \in C) \to x \in B)$
16		olc	$⊢ x \in B \to (x \in A \lor x \in B)$
17	15 16	e1a	$⊢ ((x \in B \land \neg x \in C) \to (x \in A \lor x \in B))$
18		simpr	$⊢ (x \in B \land \neg x \in C) \to \neg x \in C$
19	13 18	e1a	$⊢ ((x \in B \land \neg x \in C) \to \neg x \in C)$
20		orc	$⊢ \neg x \in C \to (\neg x \in C \lor x \in A)$
21	19 20	e1a	$⊢ ((x \in B \land \neg x \in C) \to (\neg x \in C \lor x \in A))$
22	17 21 10	e11	$⊢ ((x \in B \land \neg x \in C) \to ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A)))$
23	22	in1	$⊢ (x \in B \land \neg x \in C) \to ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
24	12 23	jaoi	$⊢ (x \in A \lor (x \in B \land \neg x \in C)) \to ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
25		anddi	$⊢ ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A)) \leftrightarrow (((x \in A \land \neg x \in C) \lor (x \in A \land x \in A)) \lor ((x \in B \land \neg x \in C) \lor (x \in B \land x \in A)))$
26	25	bicomi	$⊢ (((x \in A \land \neg x \in C) \lor (x \in A \land x \in A)) \lor ((x \in B \land \neg x \in C) \lor (x \in B \land x \in A))) \leftrightarrow ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
27		idn1	$⊢ ((x \in A \land \neg x \in C) \to (x \in A \land \neg x \in C))$
28		simpl	$⊢ (x \in A \land \neg x \in C) \to x \in A$
29	28	orcd	$⊢ (x \in A \land \neg x \in C) \to (x \in A \lor (x \in B \land \neg x \in C))$
30	27 29	e1a	$⊢ ((x \in A \land \neg x \in C) \to (x \in A \lor (x \in B \land \neg x \in C)))$
31	30	in1	$⊢ (x \in A \land \neg x \in C) \to (x \in A \lor (x \in B \land \neg x \in C))$
32		idn1	$⊢ ((x \in A \land x \in A) \to (x \in A \land x \in A))$
33		simpl	$⊢ (x \in A \land x \in A) \to x \in A$
34	32 33	e1a	$⊢ ((x \in A \land x \in A) \to x \in A)$
35		orc	$⊢ x \in A \to (x \in A \lor (x \in B \land \neg x \in C))$
36	34 35	e1a	$⊢ ((x \in A \land x \in A) \to (x \in A \lor (x \in B \land \neg x \in C)))$
37	36	in1	$⊢ (x \in A \land x \in A) \to (x \in A \lor (x \in B \land \neg x \in C))$
38	31 37	jaoi	$⊢ ((x \in A \land \neg x \in C) \lor (x \in A \land x \in A)) \to (x \in A \lor (x \in B \land \neg x \in C))$
39		olc	$⊢ (x \in B \land \neg x \in C) \to (x \in A \lor (x \in B \land \neg x \in C))$
40	13 39	e1a	$⊢ ((x \in B \land \neg x \in C) \to (x \in A \lor (x \in B \land \neg x \in C)))$
41	40	in1	$⊢ (x \in B \land \neg x \in C) \to (x \in A \lor (x \in B \land \neg x \in C))$
42		idn1	$⊢ ((x \in B \land x \in A) \to (x \in B \land x \in A))$
43		simpr	$⊢ (x \in B \land x \in A) \to x \in A$
44	42 43	e1a	$⊢ ((x \in B \land x \in A) \to x \in A)$
45	44 35	e1a	$⊢ ((x \in B \land x \in A) \to (x \in A \lor (x \in B \land \neg x \in C)))$
46	45	in1	$⊢ (x \in B \land x \in A) \to (x \in A \lor (x \in B \land \neg x \in C))$
47	41 46	jaoi	$⊢ ((x \in B \land \neg x \in C) \lor (x \in B \land x \in A)) \to (x \in A \lor (x \in B \land \neg x \in C))$
48	38 47	jaoi	$⊢ (((x \in A \land \neg x \in C) \lor (x \in A \land x \in A)) \lor ((x \in B \land \neg x \in C) \lor (x \in B \land x \in A))) \to (x \in A \lor (x \in B \land \neg x \in C))$
49	26 48	sylbir	$⊢ ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A)) \to (x \in A \lor (x \in B \land \neg x \in C))$
50	24 49	impbii	$⊢ (x \in A \lor (x \in B \land \neg x \in C)) \leftrightarrow ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
51	4 50	bitri	$⊢ x \in (A \cup (B ∖ C)) \leftrightarrow ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
52		eldif	$⊢ x \in ((A \cup B) ∖ (C ∖ A)) \leftrightarrow (x \in (A \cup B) \land \neg x \in (C ∖ A))$
53		elun	$⊢ x \in (A \cup B) \leftrightarrow (x \in A \lor x \in B)$
54		eldif	$⊢ x \in (C ∖ A) \leftrightarrow (x \in C \land \neg x \in A)$
55	54	notbii	$⊢ \neg x \in (C ∖ A) \leftrightarrow \neg (x \in C \land \neg x \in A)$
56		pm4.53	$⊢ \neg (x \in C \land \neg x \in A) \leftrightarrow (\neg x \in C \lor x \in A)$
57	55 56	bitri	$⊢ \neg x \in (C ∖ A) \leftrightarrow (\neg x \in C \lor x \in A)$
58	53 57	anbi12i	$⊢ (x \in (A \cup B) \land \neg x \in (C ∖ A)) \leftrightarrow ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
59	52 58	bitri	$⊢ x \in ((A \cup B) ∖ (C ∖ A)) \leftrightarrow ((x \in A \lor x \in B) \land (\neg x \in C \lor x \in A))$
60	51 59	bitr4i	$⊢ x \in (A \cup (B ∖ C)) \leftrightarrow x \in ((A \cup B) ∖ (C ∖ A))$
61	60	ax-gen	$⊢ \forall x (x \in (A \cup (B ∖ C)) \leftrightarrow x \in ((A \cup B) ∖ (C ∖ A)))$
62		dfcleq	$⊢ A \cup (B ∖ C) = (A \cup B) ∖ (C ∖ A) \leftrightarrow \forall x (x \in (A \cup (B ∖ C)) \leftrightarrow x \in ((A \cup B) ∖ (C ∖ A)))$
63	62	biimpri	$⊢ \forall x (x \in (A \cup (B ∖ C)) \leftrightarrow x \in ((A \cup B) ∖ (C ∖ A))) \to A \cup (B ∖ C) = (A \cup B) ∖ (C ∖ A)$
64	61 63	e0a	$⊢ A \cup (B ∖ C) = (A \cup B) ∖ (C ∖ A)$

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 ) )

Metamath Proof Explorer

Theorem undif3VD

Proof