Theorem mpompt 7560

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {csn 4588  ⟨cop 4838  ∪ ciun 4954   ↦ cmpt 5190   × cxp 5654   ∈ cmpo 7448

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-iun 4956  df-opab 5172  df-mpt 5191  df-xp 5662  df-rel 5663  df-oprab 7450  df-mpo 7451

This theorem is used by:  fconstmpo  7563  fnov  7577  fmpoco  8135  fimaproj  8182  curfv  8923  xpf1o  9189  resfval2  18100  idfusubc0  18106  catcisolem  18317  xpccatid  18394  curf2ndf  18453  evlslem4  22418  mdetunilem9  22968  txbas  23919  cnmpt1st  24020  cnmpt2nd  24021  cnmpt2c  24022  cnmpt2t  24025  txhmeo  24155  txswaphmeolem  24156  ptuncnv  24159  ptunhmeo  24160  xpstopnlem1  24161  xkohmeo  24167  prdstmdd  24476  ucnimalem  24631  fmucndlem  24642  fsum2cn  25225  conjga  33807  elrgspnlem2  33880  mplvrpmga  34260  aks6d1c2p1  43371  aks6d1c3  43376  aks6d1c4  43377  aks6d1c6lem2  43424  aks6d1c6lem4  43426  aks6d1c7lem1  43433  fmpocos  43491  lmod1zr  49820  2arymaptf  49979  iinfssclem1  50383  idfudiag1  50875