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

Theorem mpt2mpt 7029
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:   𝑥,𝑦,𝑧,𝐴   𝑦,𝐵,𝑧   𝑥,𝐶,𝑦   𝑧,𝐷   𝑥,𝐵
Allowed substitution hints:   𝐶(𝑧)   𝐷(𝑥,𝑦)

Proof of Theorem mpt2mpt
StepHypRef Expression
1 iunxpconst 5421 . . 3 𝑥𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
21mpteq1i 4974 . 2 (𝑧 𝑥𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶)
3 mpt2mpt.1 . . 3 (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)
43mpt2mptx 7028 . 2 (𝑧 𝑥𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
52, 4eqtr3i 2804 1 (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1601  {csn 4398  cop 4404   ciun 4753  cmpt 4965   × cxp 5353  cmpt2 6924
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pr 5138
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-iun 4755  df-opab 4949  df-mpt 4966  df-xp 5361  df-rel 5362  df-oprab 6926  df-mpt2 6927
This theorem is referenced by:  fconstmpt2  7032  fnov  7045  fmpt2co  7541  xpf1o  8410  resfval2  16938  catcisolem  17141  xpccatid  17214  curf2ndf  17273  evlslem4  19904  mdetunilem9  20831  txbas  21779  cnmpt1st  21880  cnmpt2nd  21881  cnmpt2c  21882  cnmpt2t  21885  txhmeo  22015  txswaphmeolem  22016  ptuncnv  22019  ptunhmeo  22020  xpstopnlem1  22021  xkohmeo  22027  prdstmdd  22335  ucnimalem  22492  fmucndlem  22503  fsum2cn  23082  fimaproj  30498  curfv  34014  idfusubc0  42880  lmod1zr  43297
  Copyright terms: Public domain W3C validator