Theorem mpoeq3ia 7497

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ⊤wtru 1571   ∈ wcel 2146   ∈ cmpo 7421

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-oprab 7423  df-mpo 7424

This theorem is used by:  mpodifsnif  7534  mposnif  7535  oprab2co  8098  cnfcomlem  9675  cnfcom2  9678  dfioo2  13495  elovmpowrd  14615  sadcom  16545  comfffval2  17781  oppchomf  17800  symgga  19523  oppglsm  19758  dfrhm2  20604  cnfldsub  21602  cnflddiv  21604  mat0op  22628  mattpos1  22665  mdetunilem7  22827  madufval  22846  maducoeval2  22849  madugsum  22852  mp2pm2mplem5  23019  mp2pm2mp  23020  leordtval  23422  xpstopnlem1  24019  divcn  25080  oprpiece1res1  25163  oprpiece1res2  25164  ehl1eudis  25632  ehl2eudis  25634  cxpcn  26963  cnnvm  31107  issply  34017  mdetpmtr2  34280  madjusmdetlem1  34283  cnre2csqima  34367  mndpluscn  34382  raddcn  34385  icorempo  38056  matunitlindflem1  38326  mendplusgfval  43968  hoidmv1le  47368  hspdifhsp  47390  vonn0ioo  47461  vonn0icc  47462  dflinc2  49249  cofuoppf  49987  dfswapf2  50098  diag1a  50142  funcsetc1o  50334