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

Theorem mpt20 6429
Description: A mapping operation with empty domain. (Contributed by Stefan O'Rear, 29-Jan-2015.) (Revised by Mario Carneiro, 15-May-2015.)
Assertion
Ref Expression
mpt20  |-  ( x  e.  (/) ,  y  e.  B  |->  C )  =  (/)

Proof of Theorem mpt20
Dummy variables  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-mpt2 6088 . 2  |-  ( x  e.  (/) ,  y  e.  B  |->  C )  =  { <. <. x ,  y
>. ,  z >.  |  ( ( x  e.  (/)  /\  y  e.  B
)  /\  z  =  C ) }
2 df-oprab 6087 . 2  |-  { <. <.
x ,  y >. ,  z >.  |  ( ( x  e.  (/)  /\  y  e.  B )  /\  z  =  C ) }  =  {
w  |  E. x E. y E. z ( w  =  <. <. x ,  y >. ,  z
>.  /\  ( ( x  e.  (/)  /\  y  e.  B )  /\  z  =  C ) ) }
3 noel 3634 . . . . . . 7  |-  -.  x  e.  (/)
4 simprll 740 . . . . . . 7  |-  ( ( w  =  <. <. x ,  y >. ,  z
>.  /\  ( ( x  e.  (/)  /\  y  e.  B )  /\  z  =  C ) )  ->  x  e.  (/) )
53, 4mto 170 . . . . . 6  |-  -.  (
w  =  <. <. x ,  y >. ,  z
>.  /\  ( ( x  e.  (/)  /\  y  e.  B )  /\  z  =  C ) )
65nex 1565 . . . . 5  |-  -.  E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\  ( ( x  e.  (/)  /\  y  e.  B
)  /\  z  =  C ) )
76nex 1565 . . . 4  |-  -.  E. y E. z ( w  =  <. <. x ,  y
>. ,  z >.  /\  ( ( x  e.  (/)  /\  y  e.  B
)  /\  z  =  C ) )
87nex 1565 . . 3  |-  -.  E. x E. y E. z
( w  =  <. <.
x ,  y >. ,  z >.  /\  (
( x  e.  (/)  /\  y  e.  B )  /\  z  =  C ) )
98abf 3663 . 2  |-  { w  |  E. x E. y E. z ( w  = 
<. <. x ,  y
>. ,  z >.  /\  ( ( x  e.  (/)  /\  y  e.  B
)  /\  z  =  C ) ) }  =  (/)
101, 2, 93eqtri 2462 1  |-  ( x  e.  (/) ,  y  e.  B  |->  C )  =  (/)
Colors of variables: wff set class
Syntax hints:    /\ wa 360   E.wex 1551    = wceq 1653    e. wcel 1726   {cab 2424   (/)c0 3630   <.cop 3819   {coprab 6084    e. cmpt2 6085
This theorem is referenced by:  homffval  13919  comfffval  13926  natfval  14145  coafval  14221  xpchomfval  14278  xpccofval  14281  meet0  14566  join0  14567  plusffval  14704  grpsubfval  14849  oppglsm  15278  dvrfval  15791  scaffval  15970  psrmulr  16450  ipffval  16881  pcofval  19037  mendplusgfval  27472  mendmulrfval  27474  mendvscafval  27477
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-dif 3325  df-in 3329  df-ss 3336  df-nul 3631  df-oprab 6087  df-mpt2 6088
  Copyright terms: Public domain W3C validator