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

Theorem mpompt 7475
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
mpompt.1 (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)
Assertion
Ref Expression
mpompt (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑦,𝐵,𝑧   𝑥,𝐶,𝑦   𝑧,𝐷   𝑥,𝐵
Allowed substitution hints:   𝐶(𝑧)   𝐷(𝑥,𝑦)

Proof of Theorem mpompt
StepHypRef Expression
1 iunxpconst 5709 . . 3 𝑥𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
21mpteq1i 5206 . 2 (𝑧 𝑥𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶)
3 mpompt.1 . . 3 (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)
43mpomptx 7474 . 2 (𝑧 𝑥𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
52, 4eqtr3i 2767 1 (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥𝐴, 𝑦𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  {csn 4591  cop 4597   ciun 4959  cmpt 5193   × cxp 5636  cmpo 7364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5261  ax-nul 5268  ax-pr 5389
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ral 3066  df-rex 3075  df-rab 3411  df-v 3450  df-sbc 3745  df-csb 3861  df-dif 3918  df-un 3920  df-in 3922  df-ss 3932  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-iun 4961  df-opab 5173  df-mpt 5194  df-xp 5644  df-rel 5645  df-oprab 7366  df-mpo 7367
This theorem is referenced by:  fconstmpo  7478  fnov  7492  fmpoco  8032  fimaproj  8072  xpf1o  9090  resfval2  17786  catcisolem  18003  xpccatid  18083  curf2ndf  18143  evlslem4  21500  mdetunilem9  21985  txbas  22934  cnmpt1st  23035  cnmpt2nd  23036  cnmpt2c  23037  cnmpt2t  23040  txhmeo  23170  txswaphmeolem  23171  ptuncnv  23174  ptunhmeo  23175  xpstopnlem1  23176  xkohmeo  23182  prdstmdd  23491  ucnimalem  23648  fmucndlem  23659  fsum2cn  24250  curfv  36087  aks6d1c2p1  40577  idfusubc0  46237  lmod1zr  46648  2arymaptf  46812
  Copyright terms: Public domain W3C validator