Theorem mpoeq3ia 7232

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537  ⊤wtru 1538   ∈ wcel 2114   ∈ cmpo 7158

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 1970  ax-7 2015  ax-9 2124  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-oprab 7160  df-mpo 7161

This theorem is referenced by:  mpodifsnif  7267  mposnif  7268  oprab2co  7792  cnfcomlem  9162  cnfcom2  9165  dfioo2  12839  elovmpowrd  13910  sadcom  15812  comfffval2  16971  oppchomf  16990  symgga  18535  oppglsm  18767  dfrhm2  19469  cnfldsub  20573  cnflddiv  20575  mat0op  21028  mattpos1  21065  mdetunilem7  21227  madufval  21246  maducoeval2  21249  madugsum  21252  mp2pm2mplem5  21418  mp2pm2mp  21419  leordtval  21821  xpstopnlem1  22417  divcn  23476  oprpiece1res1  23555  oprpiece1res2  23556  ehl1eudis  24023  ehl2eudis  24025  cxpcn  25326  cnnvm  28459  mdetpmtr2  31089  madjusmdetlem1  31092  cnre2csqima  31154  mndpluscn  31169  raddcn  31172  icorempo  34635  matunitlindflem1  34903  mendplusgfval  39834  hoidmv1le  42925  hspdifhsp  42947  vonn0ioo  43018  vonn0icc  43019  dflinc2  44514