Theorem mpompt 7506

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

Syntax hints:   → wi 4   = wceq 1540  {csn 4592  ⟨cop 4598  ∪ ciun 4958   ↦ cmpt 5191   × cxp 5639   ∈ cmpo 7392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-iun 4960  df-opab 5173  df-mpt 5192  df-xp 5647  df-rel 5648  df-oprab 7394  df-mpo 7395

This theorem is referenced by:  fconstmpo  7509  fnov  7523  fmpoco  8077  fimaproj  8117  xpf1o  9109  resfval2  17862  idfusubc0  17868  catcisolem  18079  xpccatid  18156  curf2ndf  18215  evlslem4  21990  mdetunilem9  22514  txbas  23461  cnmpt1st  23562  cnmpt2nd  23563  cnmpt2c  23564  cnmpt2t  23567  txhmeo  23697  txswaphmeolem  23698  ptuncnv  23701  ptunhmeo  23702  xpstopnlem1  23703  xkohmeo  23709  prdstmdd  24018  ucnimalem  24174  fmucndlem  24185  fsum2cn  24769  conjga  33134  elrgspnlem2  33201  curfv  37601  aks6d1c2p1  42113  aks6d1c3  42118  aks6d1c4  42119  aks6d1c6lem2  42166  aks6d1c6lem4  42168  aks6d1c7lem1  42175  fmpocos  42229  lmod1zr  48486  2arymaptf  48645  iinfssclem1  49047  idfudiag1  49518