Theorem elex2VD

Description: Virtual deduction proof of elex2 . (Contributed by Alan Sare, 25-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	elex2VD	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 𝑥 ∈ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		idn1	⊢ (    𝐴 ∈ 𝐵    ▶    𝐴 ∈ 𝐵    )
2		idn2	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 = 𝐴    ▶    𝑥 = 𝐴    )
3		eleq1a	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
4	1 2 3	e12	⊢ (    𝐴 ∈ 𝐵    ,    𝑥 = 𝐴    ▶    𝑥 ∈ 𝐵    )
5	4	in2	⊢ (    𝐴 ∈ 𝐵    ▶    ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 )    )
6	5	gen11	⊢ (    𝐴 ∈ 𝐵    ▶    ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 )    )
7		elisset	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 𝑥 = 𝐴 )
8	1 7	e1a	⊢ (    𝐴 ∈ 𝐵    ▶    ∃ 𝑥 𝑥 = 𝐴    )
9		exim	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 𝑥 ∈ 𝐵 ) )
10	6 8 9	e11	⊢ (    𝐴 ∈ 𝐵    ▶    ∃ 𝑥 𝑥 ∈ 𝐵    )
11	10	in1	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 𝑥 ∈ 𝐵 )