Theorem mpoeq3ia 7439

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114   ∈ cmpo 7363

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-oprab 7365  df-mpo 7366

This theorem is referenced by:  mpodifsnif  7476  mposnif  7477  oprab2co  8041  cnfcomlem  9614  cnfcom2  9617  dfioo2  13397  elovmpowrd  14514  sadcom  16426  comfffval2  17661  oppchomf  17680  symgga  19376  oppglsm  19611  dfrhm2  20448  cnfldsub  21390  cnflddiv  21393  cnflddivOLD  21394  mat0op  22397  mattpos1  22434  mdetunilem7  22596  madufval  22615  maducoeval2  22618  madugsum  22621  mp2pm2mplem5  22788  mp2pm2mp  22789  leordtval  23191  xpstopnlem1  23787  divcn  24848  oprpiece1res1  24931  oprpiece1res2  24932  ehl1eudis  25400  ehl2eudis  25402  cxpcn  26725  cnnvm  30771  issply  33723  mdetpmtr2  33987  madjusmdetlem1  33990  cnre2csqima  34074  mndpluscn  34089  raddcn  34092  icorempo  37684  matunitlindflem1  37954  mendplusgfval  43630  hoidmv1le  47043  hspdifhsp  47065  vonn0ioo  47136  vonn0icc  47137  dflinc2  48901  cofuoppf  49640  dfswapf2  49751  diag1a  49795  funcsetc1o  49987