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	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )

Proof

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