Metamath Proof Explorer

Theorem elex22VD

Description: Virtual deduction proof of elex22 . (Contributed by Alan Sare, 24-Oct-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion elex22VD ⊢ A ∈ B ∧ A ∈ C → ∃ x x ∈ B ∧ x ∈ C

Proof

Step Hyp Ref Expression
1 idn1 ⊢ A ∈ B ∧ A ∈ C → A ∈ B ∧ A ∈ C
2 simpl ⊢ A ∈ B ∧ A ∈ C → A ∈ B
3 1 2 e1a ⊢ A ∈ B ∧ A ∈ C → A ∈ B
4 elisset ⊢ A ∈ B → ∃ x x = A
5 3 4 e1a ⊢ A ∈ B ∧ A ∈ C → ∃ x x = A
6 idn2 ⊢ A ∈ B ∧ A ∈ C , x = A → x = A
7 eleq1a ⊢ A ∈ B → x = A → x ∈ B
8 3 6 7 e12 ⊢ A ∈ B ∧ A ∈ C , x = A → x ∈ B
9 simpr ⊢ A ∈ B ∧ A ∈ C → A ∈ C
10 1 9 e1a ⊢ A ∈ B ∧ A ∈ C → A ∈ C
11 eleq1a ⊢ A ∈ C → x = A → x ∈ C
12 10 6 11 e12 ⊢ A ∈ B ∧ A ∈ C , x = A → x ∈ C
13 pm3.2 ⊢ x ∈ B → x ∈ C → x ∈ B ∧ x ∈ C
14 8 12 13 e22 ⊢ A ∈ B ∧ A ∈ C , x = A → x ∈ B ∧ x ∈ C
15 14 in2 ⊢ A ∈ B ∧ A ∈ C → x = A → x ∈ B ∧ x ∈ C
16 15 gen11 ⊢ A ∈ B ∧ A ∈ C → ∀ x x = A → x ∈ B ∧ x ∈ C
17 exim ⊢ ∀ x x = A → x ∈ B ∧ x ∈ C → ∃ x x = A → ∃ x x ∈ B ∧ x ∈ C
18 16 17 e1a ⊢ A ∈ B ∧ A ∈ C → ∃ x x = A → ∃ x x ∈ B ∧ x ∈ C
19 pm2.27 ⊢ ∃ x x = A → ∃ x x = A → ∃ x x ∈ B ∧ x ∈ C → ∃ x x ∈ B ∧ x ∈ C
20 5 18 19 e11 ⊢ A ∈ B ∧ A ∈ C → ∃ x x ∈ B ∧ x ∈ C
21 20 in1 ⊢ A ∈ B ∧ A ∈ C → ∃ x x ∈ B ∧ x ∈ C