Theorem mpoeq3ia 7434

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpoeq3ia.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)

Assertion

Ref	Expression
mpoeq3ia	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

Proof of Theorem mpoeq3ia

Step	Hyp	Ref	Expression
1		mpoeq3ia.1	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
2	1	3adant1 1136	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
3	2	mpoeq3dva 7433	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
4	3	mptru 1554	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  ⊤wtru 1548   ∈ wcel 2119   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  mpodifsnif  7471  mposnif  7472  oprab2co  8036  cnfcomlem  9611  cnfcom2  9614  dfioo2  13394  elovmpowrd  14511  sadcom  16423  comfffval2  17658  oppchomf  17677  symgga  19373  oppglsm  19608  dfrhm2  20445  cnfldsub  21375  cnflddiv  21377  mat0op  22402  mattpos1  22439  mdetunilem7  22601  madufval  22620  maducoeval2  22623  madugsum  22626  mp2pm2mplem5  22793  mp2pm2mp  22794  leordtval  23196  xpstopnlem1  23792  divcn  24853  oprpiece1res1  24936  oprpiece1res2  24937  ehl1eudis  25405  ehl2eudis  25407  cxpcn  26727  cnnvm  30771  issply  33745  mdetpmtr2  34008  madjusmdetlem1  34011  cnre2csqima  34095  mndpluscn  34110  raddcn  34113  icorempo  37713  matunitlindflem1  37983  mendplusgfval  43626  hoidmv1le  47037  hspdifhsp  47059  vonn0ioo  47130  vonn0icc  47131  dflinc2  48901  cofuoppf  49640  dfswapf2  49751  diag1a  49795  funcsetc1o  49987