Theorem 0nelelxp

Description: A member of a Cartesian product (ordered pair) doesn't contain the empty set. (Contributed by NM, 15-Dec-2008)

	Ref	Expression
Assertion	0nelelxp	|- ( C e. ( A X. B ) -> -. (/) e. C )

Proof

Step	Hyp	Ref	Expression
1		elxp	|- ( C e. ( A X. B ) <-> E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
2		0nelop	|- -. (/) e. <. x , y >.
3		eleq2	|- ( C = <. x , y >. -> ( (/) e. C <-> (/) e. <. x , y >. ) )
4	2 3	mtbiri	|- ( C = <. x , y >. -> -. (/) e. C )
5	4	adantr	|- ( ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) -> -. (/) e. C )
6	5	exlimivv	|- ( E. x E. y ( C = <. x , y >. /\ ( x e. A /\ y e. B ) ) -> -. (/) e. C )
7	1 6	sylbi	|- ( C e. ( A X. B ) -> -. (/) e. C )