Theorem mpompt 7534

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {csn 4584  ⟨cop 4834  ∪ ciun 4950   ↦ cmpt 5185   × cxp 5648   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-iun 4952  df-opab 5167  df-mpt 5186  df-xp 5656  df-rel 5657  df-oprab 7424  df-mpo 7425

This theorem is used by:  fconstmpo  7537  fnov  7551  fmpoco  8107  fimaproj  8154  curfv  8895  xpf1o  9161  resfval2  18073  idfusubc0  18079  catcisolem  18290  xpccatid  18367  curf2ndf  18426  evlslem4  22390  mdetunilem9  22940  txbas  23891  cnmpt1st  23992  cnmpt2nd  23993  cnmpt2c  23994  cnmpt2t  23997  txhmeo  24127  txswaphmeolem  24128  ptuncnv  24131  ptunhmeo  24132  xpstopnlem1  24133  xkohmeo  24139  prdstmdd  24448  ucnimalem  24603  fmucndlem  24614  fsum2cn  25197  conjga  33777  elrgspnlem2  33850  mplvrpmga  34223  aks6d1c2p1  43261  aks6d1c3  43266  aks6d1c4  43267  aks6d1c6lem2  43314  aks6d1c6lem4  43316  aks6d1c7lem1  43323  fmpocos  43380  lmod1zr  49698  2arymaptf  49857  iinfssclem1  50261  idfudiag1  50753