Theorem mpompt 7537

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

Step	Hyp	Ref	Expression
1		iunxpconst 5739	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
2	1	mpteq1i 5207	. 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶)
3		mpompt.1	. . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)
4	3	mpomptx 7536	. 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
5	2, 4	eqtr3i 2791	1 ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {csn 4594  ⟨cop 4600  ∪ ciun 4961   ↦ cmpt 5197   × cxp 5664   ∈ cmpo 7425

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-iun 4963  df-opab 5179  df-mpt 5198  df-xp 5672  df-rel 5673  df-oprab 7427  df-mpo 7428

This theorem is used by:  fconstmpo  7540  fnov  7554  fmpoco  8099  fimaproj  8140  xpf1o  9137  resfval2  17975  idfusubc0  17981  catcisolem  18192  xpccatid  18269  curf2ndf  18328  evlslem4  22264  mdetunilem9  22814  txbas  23761  cnmpt1st  23862  cnmpt2nd  23863  cnmpt2c  23864  cnmpt2t  23867  txhmeo  23997  txswaphmeolem  23998  ptuncnv  24001  ptunhmeo  24002  xpstopnlem1  24003  xkohmeo  24009  prdstmdd  24318  ucnimalem  24473  fmucndlem  24484  fsum2cn  25067  conjga  33521  elrgspnlem2  33594  mplvrpmga  33966  curfv  38292  aks6d1c2p1  42926  aks6d1c3  42931  aks6d1c4  42932  aks6d1c6lem2  42979  aks6d1c6lem4  42981  aks6d1c7lem1  42988  fmpocos  43045  lmod1zr  49314  2arymaptf  49473  iinfssclem1  49873  idfudiag1  50344