Theorem 0nelxp 5380

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	⊢ ¬ ∅ ∈ (𝐴 × 𝐵)

Proof of Theorem 0nelxp

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3417	. . . . . . 7 ⊢ 𝑥 ∈ V
2		vex 3417	. . . . . . 7 ⊢ 𝑦 ∈ V
3	1, 2	opnzi 5165	. . . . . 6 ⊢ ⟨𝑥, 𝑦⟩ ≠ ∅
4	3	nesymi 3056	. . . . 5 ⊢ ¬ ∅ = ⟨𝑥, 𝑦⟩
5	4	intnanr 483	. . . 4 ⊢ ¬ (∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
6	5	nex 1899	. . 3 ⊢ ¬ ∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
7	6	nex 1899	. 2 ⊢ ¬ ∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵))
8		elxp 5369	. 2 ⊢ (∅ ∈ (𝐴 × 𝐵) ↔ ∃𝑥∃𝑦(∅ = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)))
9	7, 8	mtbir 315	1 ⊢ ¬ ∅ ∈ (𝐴 × 𝐵)

Syntax hints:  ¬ wn 3   ∧ wa 386   = wceq 1656  ∃wex 1878   ∈ wcel 2164  ∅c0 4146  ⟨cop 4405   × cxp 5344

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pr 5129

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4147  df-if 4309  df-sn 4400  df-pr 4402  df-op 4406  df-opab 4938  df-xp 5352

This theorem is referenced by:  0nelrel  5401  nrelv  5462  dmsn0  5847  onxpdisj  6086  nfunv  6160  mpt2xopx0ov0  7612  reldmtpos  7630  dmtpos  7634  0nnq  10068  adderpq  10100  mulerpq  10101  lterpq  10114  0ncn  10277  structcnvcnv  16243  vtxval0  26344  iedgval0  26345  msrrcl  31982  relintabex  38727