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

Theorem 0xp 5073
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 5011 . . 3  |-  ( z  e.  ( (/)  X.  A
)  <->  E. x E. y
( z  =  <. x ,  y >.  /\  (
x  e.  (/)  /\  y  e.  A ) ) )
2 noel 3784 . . . . . . 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 1605 . . . . 5  |-  -.  E. y ( z  = 
<. x ,  y >.  /\  ( x  e.  (/)  /\  y  e.  A ) )
65nex 1605 . . . 4  |-  -.  E. x E. y ( z  =  <. x ,  y
>.  /\  ( x  e.  (/)  /\  y  e.  A
) )
7 noel 3784 . . . 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 2458 1  |-  ( (/)  X.  A )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 369    = wceq 1374   E.wex 1591    e. wcel 1762   (/)c0 3780   <.cop 4028    X. cxp 4992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-sep 4563  ax-nul 4571  ax-pr 4681
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-v 3110  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3781  df-if 3935  df-sn 4023  df-pr 4025  df-op 4029  df-opab 4501  df-xp 5000
This theorem is referenced by:  dmxpid  5215  csbres  5269  res0  5271  xp0  5418  xpnz  5419  xpdisj1  5421  difxp2  5426  xpcan2  5437  xpima  5442  unixp  5533  unixpid  5535  xpcoid  5541  fodomr  7660  xpfi  7782  cdaassen  8553  iundom2g  8906  alephadd  8943  hashxplem  12446  ramcl  14397  mat0dimbas0  18730  mavmul0g  18817  txindislem  19864  txhaus  19878  tmdgsum  20324  ust0  20452  sibf0  27904  0mbf  29626
  Copyright terms: Public domain W3C validator