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

Theorem mpt2mpt 6152
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
Assertion
Ref Expression
mpt2mpt
Distinct variable groups:   , , ,   , ,   , ,   ,   ,

Proof of Theorem mpt2mpt
StepHypRef Expression
1 iunxpconst 4866 . . 3
2 mpteq1 4347 . . 3
31, 2ax-mp 5 . 2
4 mpt2mpt.1 . . 3
54mpt2mptx 6151 . 2
63, 5eqtr3i 2444 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1687  {csn 3853  <.cop 3856  U_ciun 4146  e.cmpt 4325  X.cxp 4809  e.cmpt2 6063
This theorem is referenced by:  fconstmpt2  6155  fnov  6168  fmpt2co  6625  xpf1o  7432  resfval2  14743  catcisolem  14914  xpccatid  14938  curf2ndf  14997  evlslem4  17388  mdetunilem9  18128  txbas  18844  cnmpt1st  18945  cnmpt2nd  18946  cnmpt2c  18947  cnmpt2t  18950  txhmeo  19080  txswaphmeolem  19081  ptuncnv  19084  ptunhmeo  19085  xpstopnlem1  19086  xkohmeo  19092  prdstmdd  19398  ucnimalem  19555  fmucndlem  19566  fsum2cn  20147  lmod1zr  30619
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pr 4503
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-ral 2699  df-rex 2700  df-rab 2703  df-v 2953  df-sbc 3165  df-csb 3266  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-iun 4148  df-opab 4326  df-mpt 4327  df-xp 4817  df-rel 4818  df-oprab 6065  df-mpt2 6066
  Copyright terms: Public domain W3C validator