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

Theorem 0xp 4915
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 4851 . . 3  |-  ( z  e.  ( (/)  X.  A
)  <->  E. x E. y
( z  =  <. x ,  y >.  /\  (
x  e.  (/)  /\  y  e.  A ) ) )
2 noel 3735 . . . . . . 7  |-  -.  x  e.  (/)
3 simprl 764 . . . . . . 7  |-  ( ( z  =  <. x ,  y >.  /\  (
x  e.  (/)  /\  y  e.  A ) )  ->  x  e.  (/) )
42, 3mto 180 . . . . . 6  |-  -.  (
z  =  <. x ,  y >.  /\  (
x  e.  (/)  /\  y  e.  A ) )
54nex 1678 . . . . 5  |-  -.  E. y ( z  = 
<. x ,  y >.  /\  ( x  e.  (/)  /\  y  e.  A ) )
65nex 1678 . . . 4  |-  -.  E. x E. y ( z  =  <. x ,  y
>.  /\  ( x  e.  (/)  /\  y  e.  A
) )
7 noel 3735 . . . 4  |-  -.  z  e.  (/)
86, 72false 352 . . 3  |-  ( E. x E. y ( z  =  <. x ,  y >.  /\  (
x  e.  (/)  /\  y  e.  A ) )  <->  z  e.  (/) )
91, 8bitri 253 . 2  |-  ( z  e.  ( (/)  X.  A
)  <->  z  e.  (/) )
109eqriv 2448 1  |-  ( (/)  X.  A )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    /\ wa 371    = wceq 1444   E.wex 1663    e. wcel 1887   (/)c0 3731   <.cop 3974    X. cxp 4832
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-opab 4462  df-xp 4840
This theorem is referenced by:  dmxpid  5054  csbres  5108  res0  5109  xp0  5255  xpnz  5256  xpdisj1  5258  difxp2  5263  xpcan2  5274  xpima  5279  unixp  5369  unixpid  5371  xpcoid  5377  fodomr  7723  xpfi  7842  cdaassen  8612  iundom2g  8965  alephadd  9002  hashxplem  12605  dmtrclfv  13082  ramcl  14987  0subcat  15743  mat0dimbas0  19491  mavmul0g  19578  txindislem  20648  txhaus  20662  tmdgsum  21110  ust0  21234  sibf0  29167  mexval2  30141  poimirlem5  31945  poimirlem10  31950  poimirlem22  31962  poimirlem23  31963  poimirlem26  31966  poimirlem28  31968  0mbf  31986  0heALT  36379
  Copyright terms: Public domain W3C validator