Theorem 0nelxp 5143

Description: The empty set is not a member of a Cartesian product. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 26-Apr-2015.) (Proof shortened by JJ, 13-Aug-2021.)

Assertion

Ref	Expression
0nelxp	|- -. (/) e. ( A X. B )

Proof of Theorem 0nelxp

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3203	. . . . . . 7 |- x e. _V
2		vex 3203	. . . . . . 7 |- y e. _V
3	1, 2	opnzi 4943	. . . . . 6 |- <. x , y >. =/= (/)
4	3	nesymi 2851	. . . . 5 |- -. (/) = <. x , y >.
5	4	intnanr 961	. . . 4 |- -. ( (/) = <. x , y >. /\ ( x e. A /\ y e. B ) )
6	5	nex 1731	. . 3 |- -. E. y ( (/) = <. x , y >. /\ ( x e. A /\ y e. B ) )
7	6	nex 1731	. 2 |- -. E. x E. y ( (/) = <. x , y >. /\ ( x e. A /\ y e. B ) )
8		elxp 5131	. 2 |- ( (/) e. ( A X. B ) <-> E. x E. y ( (/) = <. x , y >. /\ ( x e. A /\ y e. B ) ) )
9	7, 8	mtbir 313	1 |- -. (/) e. ( A X. B )

Syntax hints:   -. wn 3   /\ wa 384   = wceq 1483   E.wex 1704   e. wcel 1990   (/)c0 3915   <.cop 4183   X. cxp 5112

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-xp 5120

This theorem is referenced by:  0nelrel  5162  nrelv  5244  dmsn0  5602  onxpdisj  5847  nfunv  5921  mpt2xopx0ov0  7342  reldmtpos  7360  dmtpos  7364  0nnq  9746  adderpq  9778  mulerpq  9779  lterpq  9792  0ncn  9954  structcnvcnv  15871  vtxval0  25931  iedgval0  25932  msrrcl  31440  relintabex  37887