MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  0xp Structured version   Unicode version

Theorem 0xp 4916
Description: The Cartesian product with the empty set is empty. Part of Theorem 3.13(ii) of [Monk1] p. 37. (Contributed by NM, 4-Jul-1994.)
Assertion
Ref Expression
0xp  |-  ( (/)  X.  A )  =  (/)

Proof of Theorem 0xp
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp 4856 . . 3  |-  ( z  e.  ( (/)  X.  A
)  <->  E. x E. y
( z  =  <. x ,  y >.  /\  (
x  e.  (/)  /\  y  e.  A ) ) )
2 noel 3640 . . . . . . 7  |-  -.  x  e.  (/)
3 simprl 755 . . . . . . 7  |-  ( ( z  =  <. x ,  y >.  /\  (
x  e.  (/)  /\  y  e.  A ) )  ->  x  e.  (/) )
42, 3mto 176 . . . . . 6  |-  -.  (
z  =  <. x ,  y >.  /\  (
x  e.  (/)  /\  y  e.  A ) )
54nex 1600 . . . . 5  |-  -.  E. y ( z  = 
<. x ,  y >.  /\  ( x  e.  (/)  /\  y  e.  A ) )
65nex 1600 . . . 4  |-  -.  E. x E. y ( z  =  <. x ,  y
>.  /\  ( x  e.  (/)  /\  y  e.  A
) )
7 noel 3640 . . . 4  |-  -.  z  e.  (/)
86, 72false 350 . . 3  |-  ( E. x E. y ( z  =  <. x ,  y >.  /\  (
x  e.  (/)  /\  y  e.  A ) )  <->  z  e.  (/) )
91, 8bitri 249 . 2  |-  ( z  e.  ( (/)  X.  A
)  <->  z  e.  (/) )
109eqriv 2439 1  |-  ( (/)  X.  A )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1369   E.wex 1586    e. wcel 1756   (/)c0 3636   <.cop 3882    X. cxp 4837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4412  ax-nul 4420  ax-pr 4530
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-ne 2607  df-v 2973  df-dif 3330  df-un 3332  df-in 3334  df-ss 3341  df-nul 3637  df-if 3791  df-sn 3877  df-pr 3879  df-op 3883  df-opab 4350  df-xp 4845
This theorem is referenced by:  dmxpid  5058  csbres  5112  res0  5114  xp0  5255  xpnz  5256  xpdisj1  5258  difxp2  5263  xpcan2  5274  xpima  5279  unixp  5369  unixpid  5371  xpcoid  5377  fodomr  7461  xpfi  7582  cdaassen  8350  iundom2g  8703  alephadd  8740  hashxplem  12194  ramcl  14089  mat0dimbas0  18324  mavmul0g  18363  txindislem  19205  txhaus  19219  tmdgsum  19665  ust0  19793  sibf0  26719  0mbf  28435
  Copyright terms: Public domain W3C validator