This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem csbingVD

Description: Virtual deduction proof of csbin . 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. csbin is csbingVD without virtual deductions and was automatically derived from csbingVD .

1:: |- (. A e. B ->. A e. B ).
2:: |- ( C i^i D ) = { y | ( y e. C /\ y e. D ) }
20:2: |- A. x ( C i^i D ) = { y | ( y e. C /\ y e. D ) }
30:1,20: |- (. A e. B ->. [. A / x ]. ( C i^i D ) = { y | ( y e. C /\ y e. D ) } ).
3:1,30: |- (. A e. B ->. [_ A / x ]_ ( C i^i D ) = [_ A / x ]_ { y | ( y e. C /\ y e. D ) } ).
4:1: |- (. A e. B ->. [_ A / x ]_ { y | ( y e. C /\ y e. D ) } = { y | [. A / x ]. ( y e. C /\ y e. D ) } ).
5:3,4: |- (. A e. B ->. [_ A / x ]_ ( C i^i D ) = { y | [. A / x ]. ( y e. C /\ y e. D ) } ).
6:1: |- (. A e. B ->. ( [. A / x ]. y e. C <-> y e. [_ A / x ]_ C ) ).
7:1: |- (. A e. B ->. ( [. A / x ]. y e. D <-> y e. [_ A / x ]_ D ) ).
8:6,7: |- (. A e. B ->. ( ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ).
9:1: |- (. A e. B ->. ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( [. A / x ]. y e. C /\ [. A / x ]. y e. D ) ) ).
10:9,8: |- (. A e. B ->. ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ).
11:10: |- (. A e. B ->. A. y ( [. A / x ]. ( y e. C /\ y e. D ) <-> ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) ) ).
12:11: |- (. A e. B ->. { y | [. A / x ]. ( y e. C /\ y e. D ) } = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } ).
13:5,12: |- (. A e. B ->. [_ A / x ]_ ( C i^i D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) } ).
14:: |- ( [_ A / x ]_ C i^i [_ A / x ]_ D ) = { y | ( y e. [_ A / x ]_ C /\ y e. [_ A / x ]_ D ) }
15:13,14: |- (. A e. B ->. [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) ).
qed:15: |- ( A e. B -> [_ A / x ]_ ( C i^i D ) = ( [_ A / x ]_ C i^i [_ A / x ]_ D ) )
(Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion csbingVD ⊢ A ∈ B → ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ C ∩ ⦋ A / x⦌ D

Proof

Step Hyp Ref Expression
1 idn1 ⊢ A ∈ B → A ∈ B
2 df-in ⊢ C ∩ D = y | y ∈ C ∧ y ∈ D
3 2 ax-gen ⊢ ∀ x C ∩ D = y | y ∈ C ∧ y ∈ D
4 spsbc ⊢ A ∈ B → ∀ x C ∩ D = y | y ∈ C ∧ y ∈ D → [˙A / x]˙ C ∩ D = y | y ∈ C ∧ y ∈ D
5 1 3 4 e10 ⊢ A ∈ B → [˙A / x]˙ C ∩ D = y | y ∈ C ∧ y ∈ D
6 sbceqg ⊢ A ∈ B → [˙A / x]˙ C ∩ D = y | y ∈ C ∧ y ∈ D ↔ ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D
7 6 biimpd ⊢ A ∈ B → [˙A / x]˙ C ∩ D = y | y ∈ C ∧ y ∈ D → ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D
8 1 5 7 e11 ⊢ A ∈ B → ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D
9 csbab ⊢ ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D
10 9 a1i ⊢ A ∈ B → ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D
11 1 10 e1a ⊢ A ∈ B → ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D
12 eqeq1 ⊢ ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D → ⦋ A / x⦌ C ∩ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D
13 12 biimprd ⊢ ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D → ⦋ A / x⦌ y | y ∈ C ∧ y ∈ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D → ⦋ A / x⦌ C ∩ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D
14 8 11 13 e11 ⊢ A ∈ B → ⦋ A / x⦌ C ∩ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D
15 sbcan ⊢ [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D
16 15 a1i ⊢ A ∈ B → [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D
17 1 16 e1a ⊢ A ∈ B → [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D
18 sbcel2 ⊢ [˙A / x]˙ y ∈ C ↔ y ∈ ⦋ A / x⦌ C
19 18 a1i ⊢ A ∈ B → [˙A / x]˙ y ∈ C ↔ y ∈ ⦋ A / x⦌ C
20 1 19 e1a ⊢ A ∈ B → [˙A / x]˙ y ∈ C ↔ y ∈ ⦋ A / x⦌ C
21 sbcel2 ⊢ [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ D
22 21 a1i ⊢ A ∈ B → [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ D
23 1 22 e1a ⊢ A ∈ B → [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ D
24 pm4.38 ⊢ [˙A / x]˙ y ∈ C ↔ y ∈ ⦋ A / x⦌ C ∧ [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ D → [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
25 24 ex ⊢ [˙A / x]˙ y ∈ C ↔ y ∈ ⦋ A / x⦌ C → [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ D → [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
26 20 23 25 e11 ⊢ A ∈ B → [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
27 bibi1 ⊢ [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D → [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D ↔ [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
28 27 biimprd ⊢ [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D → [˙A / x]˙ y ∈ C ∧ [˙A / x]˙ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D → [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
29 17 26 28 e11 ⊢ A ∈ B → [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
30 29 gen11 ⊢ A ∈ B → ∀ y [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
31 abbib ⊢ y | [˙A / x]˙ y ∈ C ∧ y ∈ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D ↔ ∀ y [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
32 31 biimpri ⊢ ∀ y [˙A / x]˙ y ∈ C ∧ y ∈ D ↔ y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D → y | [˙A / x]˙ y ∈ C ∧ y ∈ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
33 30 32 e1a ⊢ A ∈ B → y | [˙A / x]˙ y ∈ C ∧ y ∈ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
34 eqeq1 ⊢ ⦋ A / x⦌ C ∩ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D → ⦋ A / x⦌ C ∩ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D ↔ y | [˙A / x]˙ y ∈ C ∧ y ∈ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
35 34 biimprd ⊢ ⦋ A / x⦌ C ∩ D = y | [˙A / x]˙ y ∈ C ∧ y ∈ D → y | [˙A / x]˙ y ∈ C ∧ y ∈ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D → ⦋ A / x⦌ C ∩ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
36 14 33 35 e11 ⊢ A ∈ B → ⦋ A / x⦌ C ∩ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
37 df-in ⊢ ⦋ A / x⦌ C ∩ ⦋ A / x⦌ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
38 eqeq2 ⊢ ⦋ A / x⦌ C ∩ ⦋ A / x⦌ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D → ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ C ∩ ⦋ A / x⦌ D ↔ ⦋ A / x⦌ C ∩ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D
39 38 biimprcd ⊢ ⦋ A / x⦌ C ∩ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D → ⦋ A / x⦌ C ∩ ⦋ A / x⦌ D = y | y ∈ ⦋ A / x⦌ C ∧ y ∈ ⦋ A / x⦌ D → ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ C ∩ ⦋ A / x⦌ D
40 36 37 39 e10 ⊢ A ∈ B → ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ C ∩ ⦋ A / x⦌ D
41 40 in1 ⊢ A ∈ B → ⦋ A / x⦌ C ∩ D = ⦋ A / x⦌ C ∩ ⦋ A / x⦌ D