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

Theorem mpt2mpt 6315
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 5012 . . 3
2 mpteq1 4489 . . 3
31, 2ax-mp 5 . 2
4 mpt2mpt.1 . . 3
54mpt2mptx 6314 . 2
63, 5eqtr3i 2485 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1370  {csn 3993  <.cop 3999  U_ciun 4288  e.cmpt 4467  X.cxp 4955  e.cmpt2 6224
This theorem is referenced by:  fconstmpt2  6318  fnov  6331  fmpt2co  6789  xpf1o  7607  resfval2  14962  catcisolem  15133  xpccatid  15157  curf2ndf  15216  evlslem4OLD  17767  evlslem4  17768  mdetunilem9  18694  txbas  19539  cnmpt1st  19640  cnmpt2nd  19641  cnmpt2c  19642  cnmpt2t  19645  txhmeo  19775  txswaphmeolem  19776  ptuncnv  19779  ptunhmeo  19780  xpstopnlem1  19781  xkohmeo  19787  prdstmdd  20093  ucnimalem  20254  fmucndlem  20265  fsum2cn  20846  lmod1zr  31807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pr 4648
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3083  df-sbc 3298  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-iun 4290  df-opab 4468  df-mpt 4469  df-xp 4963  df-rel 4964  df-oprab 6226  df-mpt2 6227
  Copyright terms: Public domain W3C validator