Theorem mpoeq3ia 7511

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 1131	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
3	2	mpoeq3dva 7510	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
4	3	mptru 1547	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ⊤wtru 1541   ∈ wcel 2108   ∈ cmpo 7433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-oprab 7435  df-mpo 7436

This theorem is referenced by:  mpodifsnif  7548  mposnif  7549  oprab2co  8122  cnfcomlem  9739  cnfcom2  9742  dfioo2  13490  elovmpowrd  14596  sadcom  16500  comfffval2  17744  oppchomf  17763  symgga  19425  oppglsm  19660  dfrhm2  20474  cnfldsub  21410  cnflddiv  21413  cnflddivOLD  21414  mat0op  22425  mattpos1  22462  mdetunilem7  22624  madufval  22643  maducoeval2  22646  madugsum  22649  mp2pm2mplem5  22816  mp2pm2mp  22817  leordtval  23221  xpstopnlem1  23817  divcnOLD  24890  divcn  24892  oprpiece1res1  24982  oprpiece1res2  24983  ehl1eudis  25454  ehl2eudis  25456  cxpcn  26787  cxpcnOLD  26788  cnnvm  30701  mdetpmtr2  33823  madjusmdetlem1  33826  cnre2csqima  33910  mndpluscn  33925  raddcn  33928  icorempo  37352  matunitlindflem1  37623  mendplusgfval  43193  hoidmv1le  46609  hspdifhsp  46631  vonn0ioo  46702  vonn0icc  46703  dflinc2  48327  dfswapf2  48967