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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ⊤wtru 1542   ∈ wcel 2113   ∈ cmpo 7358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-oprab 7360  df-mpo 7361

This theorem is referenced by:  mpodifsnif  7471  mposnif  7472  oprab2co  8037  cnfcomlem  9606  cnfcom2  9609  dfioo2  13364  elovmpowrd  14479  sadcom  16388  comfffval2  17622  oppchomf  17641  symgga  19334  oppglsm  19569  dfrhm2  20408  cnfldsub  21350  cnflddiv  21353  cnflddivOLD  21354  mat0op  22361  mattpos1  22398  mdetunilem7  22560  madufval  22579  maducoeval2  22582  madugsum  22585  mp2pm2mplem5  22752  mp2pm2mp  22753  leordtval  23155  xpstopnlem1  23751  divcnOLD  24811  divcn  24813  oprpiece1res1  24903  oprpiece1res2  24904  ehl1eudis  25374  ehl2eudis  25376  cxpcn  26708  cxpcnOLD  26709  cnnvm  30706  issply  33668  mdetpmtr2  33930  madjusmdetlem1  33933  cnre2csqima  34017  mndpluscn  34032  raddcn  34035  icorempo  37495  matunitlindflem1  37756  mendplusgfval  43365  hoidmv1le  46780  hspdifhsp  46802  vonn0ioo  46873  vonn0icc  46874  dflinc2  48598  cofuoppf  49337  dfswapf2  49448  diag1a  49492  funcsetc1o  49684