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	|- ( ( A e. B /\ A e. C ) -> E. x ( x e. B /\ x e. C ) )

Proof

Step	Hyp	Ref	Expression
1		eleq1a	|- ( A e. B -> ( x = A -> x e. B ) )
2		eleq1a	|- ( A e. C -> ( x = A -> x e. C ) )
3	1 2	anim12ii	|- ( ( A e. B /\ A e. C ) -> ( x = A -> ( x e. B /\ x e. C ) ) )
4	3	alrimiv	|- ( ( A e. B /\ A e. C ) -> A. x ( x = A -> ( x e. B /\ x e. C ) ) )
5		elissetv	|- ( A e. B -> E. x x = A )
6	5	adantr	|- ( ( A e. B /\ A e. C ) -> E. x x = A )
7		exim	|- ( A. x ( x = A -> ( x e. B /\ x e. C ) ) -> ( E. x x = A -> E. x ( x e. B /\ x e. C ) ) )
8	4 6 7	sylc	|- ( ( A e. B /\ A e. C ) -> E. x ( x e. B /\ x e. C ) )