Theorem mpompt 7526

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

Syntax hints:   → wi 4   = wceq 1570  {csn 4590  ⟨cop 4596  ∪ ciun 4957   ↦ cmpt 5193   × cxp 5661   ∈ cmpo 7414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-iun 4959  df-opab 5175  df-mpt 5194  df-xp 5669  df-rel 5670  df-oprab 7416  df-mpo 7417

This theorem is referenced by:  fconstmpo  7529  fnov  7543  fmpoco  8091  fimaproj  8132  xpf1o  9128  resfval2  17951  idfusubc0  17957  catcisolem  18168  xpccatid  18245  curf2ndf  18304  evlslem4  22208  mdetunilem9  22758  txbas  23705  cnmpt1st  23806  cnmpt2nd  23807  cnmpt2c  23808  cnmpt2t  23811  txhmeo  23941  txswaphmeolem  23942  ptuncnv  23945  ptunhmeo  23946  xpstopnlem1  23947  xkohmeo  23953  prdstmdd  24262  ucnimalem  24417  fmucndlem  24428  fsum2cn  25011  conjga  33468  elrgspnlem2  33541  mplvrpmga  33913  curfv  38229  aks6d1c2p1  42863  aks6d1c3  42868  aks6d1c4  42869  aks6d1c6lem2  42916  aks6d1c6lem4  42918  aks6d1c7lem1  42925  fmpocos  42982  lmod1zr  49250  2arymaptf  49409  iinfssclem1  49809  idfudiag1  50280