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

Theorem mpt2mpt 6171
Description: Express a two-argument function as a one-argument function, or vice-versa. (Contributed by Mario Carneiro, 17-Dec-2013.) (Revised by Mario Carneiro, 29-Dec-2014.)
Hypothesis
Ref Expression
mpt2mpt.1  |-  ( z  =  <. x ,  y
>.  ->  C  =  D )
Assertion
Ref Expression
mpt2mpt  |-  ( z  e.  ( A  X.  B )  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )
Distinct variable groups:    x, y,
z, A    y, B, z    x, C, y    z, D    x, B
Allowed substitution hints:    C( z)    D( x, y)

Proof of Theorem mpt2mpt
StepHypRef Expression
1 iunxpconst 4882 . . 3  |-  U_ x  e.  A  ( {
x }  X.  B
)  =  ( A  X.  B )
2 mpteq1 4360 . . 3  |-  ( U_ x  e.  A  ( { x }  X.  B )  =  ( A  X.  B )  ->  ( z  e. 
U_ x  e.  A  ( { x }  X.  B )  |->  C )  =  ( z  e.  ( A  X.  B
)  |->  C ) )
31, 2ax-mp 5 . 2  |-  ( z  e.  U_ x  e.  A  ( { x }  X.  B )  |->  C )  =  ( z  e.  ( A  X.  B )  |->  C )
4 mpt2mpt.1 . . 3  |-  ( z  =  <. x ,  y
>.  ->  C  =  D )
54mpt2mptx 6170 . 2  |-  ( z  e.  U_ x  e.  A  ( { x }  X.  B )  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )
63, 5eqtr3i 2455 1  |-  ( z  e.  ( A  X.  B )  |->  C )  =  ( x  e.  A ,  y  e.  B  |->  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362   {csn 3865   <.cop 3871   U_ciun 4159    e. cmpt 4338    X. cxp 4825    e. cmpt2 6082
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-iun 4161  df-opab 4339  df-mpt 4340  df-xp 4833  df-rel 4834  df-oprab 6084  df-mpt2 6085
This theorem is referenced by:  fconstmpt2  6174  fnov  6187  fmpt2co  6645  xpf1o  7461  resfval2  14785  catcisolem  14956  xpccatid  14980  curf2ndf  15039  evlslem4OLD  17517  evlslem4  17518  mdetunilem9  18267  txbas  18981  cnmpt1st  19082  cnmpt2nd  19083  cnmpt2c  19084  cnmpt2t  19087  txhmeo  19217  txswaphmeolem  19218  ptuncnv  19221  ptunhmeo  19222  xpstopnlem1  19223  xkohmeo  19229  prdstmdd  19535  ucnimalem  19696  fmucndlem  19707  fsum2cn  20288  lmod1zr  30741
  Copyright terms: Public domain W3C validator