Theorem mpompt 7481

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

Syntax hints:   → wi 4   = wceq 1542  {csn 4567  ⟨cop 4573  ∪ ciun 4933   ↦ cmpt 5166   × cxp 5629   ∈ cmpo 7369

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-iun 4935  df-opab 5148  df-mpt 5167  df-xp 5637  df-rel 5638  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  fconstmpo  7484  fnov  7498  fmpoco  8045  fimaproj  8085  xpf1o  9077  resfval2  17860  idfusubc0  17866  catcisolem  18077  xpccatid  18154  curf2ndf  18213  evlslem4  22054  mdetunilem9  22585  txbas  23532  cnmpt1st  23633  cnmpt2nd  23634  cnmpt2c  23635  cnmpt2t  23638  txhmeo  23768  txswaphmeolem  23769  ptuncnv  23772  ptunhmeo  23773  xpstopnlem1  23774  xkohmeo  23780  prdstmdd  24089  ucnimalem  24244  fmucndlem  24255  fsum2cn  24838  conjga  33231  elrgspnlem2  33304  mplvrpmga  33689  curfv  37921  aks6d1c2p1  42557  aks6d1c3  42562  aks6d1c4  42563  aks6d1c6lem2  42610  aks6d1c6lem4  42612  aks6d1c7lem1  42619  fmpocos  42675  lmod1zr  48969  2arymaptf  49128  iinfssclem1  49529  idfudiag1  50000