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

Metamath Proof Explorer

Theorem en3lplem1VD

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

Ref Expression
Assertion en3lplem1VD ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = A → ∃ y y ∈ A B C ∧ y ∈ x

Proof

Step Hyp Ref Expression
1 idn1 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → A ∈ B ∧ B ∈ C ∧ C ∈ A
2 simp3 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → C ∈ A
3 1 2 e1a ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → C ∈ A
4 tpid3g ⊢ C ∈ A → C ∈ A B C
5 3 4 e1a ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → C ∈ A B C
6 idn2 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x = A → x = A
7 eleq2 ⊢ x = A → C ∈ x ↔ C ∈ A
8 7 biimprd ⊢ x = A → C ∈ A → C ∈ x
9 6 3 8 e21 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x = A → C ∈ x
10 pm3.2 ⊢ C ∈ A B C → C ∈ x → C ∈ A B C ∧ C ∈ x
11 5 9 10 e12 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x = A → C ∈ A B C ∧ C ∈ x
12 elex22 ⊢ C ∈ A B C ∧ C ∈ x → ∃ y y ∈ A B C ∧ y ∈ x
13 11 12 e2 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A , x = A → ∃ y y ∈ A B C ∧ y ∈ x
14 13 in2 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = A → ∃ y y ∈ A B C ∧ y ∈ x
15 14 in1 ⊢ A ∈ B ∧ B ∈ C ∧ C ∈ A → x = A → ∃ y y ∈ A B C ∧ y ∈ x