Theorem elex22

Description: If two classes each contain another class, then both contain some set. (Contributed by Alan Sare, 24-Oct-2011)

	Ref	Expression
Assertion	elex22	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1a	⊢ ( 𝐴 ∈ 𝐵 → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐵 ) )
2		eleq1a	⊢ ( 𝐴 ∈ 𝐶 → ( 𝑥 = 𝐴 → 𝑥 ∈ 𝐶 ) )
3	1 2	anim12ii	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) → ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
4	3	alrimiv	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) → ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
5		elissetv	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 𝑥 = 𝐴 )
6	5	adantr	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) → ∃ 𝑥 𝑥 = 𝐴 )
7		exim	⊢ ( ∀ 𝑥 ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) → ( ∃ 𝑥 𝑥 = 𝐴 → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) ) )
8	4 6 7	sylc	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ∈ 𝐶 ) → ∃ 𝑥 ( 𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶 ) )