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	$⊢ (A \in B \land A \in C) \to \exists x (x \in B \land x \in C)$

Step	Hyp	Ref	Expression
1		eleq1a	$⊢ A \in B \to (x = A \to x \in B)$
2		eleq1a	$⊢ A \in C \to (x = A \to x \in C)$
3	1 2	anim12ii	$⊢ (A \in B \land A \in C) \to (x = A \to (x \in B \land x \in C))$
4	3	alrimiv	$⊢ (A \in B \land A \in C) \to \forall x (x = A \to (x \in B \land x \in C))$
5		elisset	$⊢ A \in B \to \exists x x = A$
6	5	adantr	$⊢ (A \in B \land A \in C) \to \exists x x = A$
7		exim	$⊢ \forall x (x = A \to (x \in B \land x \in C)) \to (\exists x x = A \to \exists x (x \in B \land x \in C))$
8	4 6 7	sylc	$⊢ (A \in B \land A \in C) \to \exists x (x \in B \land x \in C)$

Metamath Proof Explorer