Theorem mpompt 7466

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 5692	. . 3 ⊢ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) = (𝐴 × 𝐵)
2	1	mpteq1i 5184	. 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶)
3		mpompt.1	. . 3 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝐶 = 𝐷)
4	3	mpomptx 7465	. 2 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)
5	2, 4	eqtr3i 2758	1 ⊢ (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   = wceq 1541  {csn 4575  ⟨cop 4581  ∪ ciun 4941   ↦ cmpt 5174   × cxp 5617   ∈ cmpo 7354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-iun 4943  df-opab 5156  df-mpt 5175  df-xp 5625  df-rel 5626  df-oprab 7356  df-mpo 7357

This theorem is referenced by:  fconstmpo  7469  fnov  7483  fmpoco  8031  fimaproj  8071  xpf1o  9059  resfval2  17802  idfusubc0  17808  catcisolem  18019  xpccatid  18096  curf2ndf  18155  evlslem4  22012  mdetunilem9  22536  txbas  23483  cnmpt1st  23584  cnmpt2nd  23585  cnmpt2c  23586  cnmpt2t  23589  txhmeo  23719  txswaphmeolem  23720  ptuncnv  23723  ptunhmeo  23724  xpstopnlem1  23725  xkohmeo  23731  prdstmdd  24040  ucnimalem  24195  fmucndlem  24206  fsum2cn  24790  conjga  33146  elrgspnlem2  33217  mplvrpmga  33593  curfv  37660  aks6d1c2p1  42231  aks6d1c3  42236  aks6d1c4  42237  aks6d1c6lem2  42284  aks6d1c6lem4  42286  aks6d1c7lem1  42293  fmpocos  42352  lmod1zr  48618  2arymaptf  48777  iinfssclem1  49179  idfudiag1  49650