Theorem mpoeq3ia 7492

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

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

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 2155  ax-ext 2732

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 2739  df-cleq 2752  df-oprab 7418  df-mpo 7419

This theorem is used by:  mpodifsnif  7529  mposnif  7530  oprab2co  8095  cnfcomlem  9681  cnfcom2  9684  dfioo2  13506  elovmpowrd  14626  sadcom  16556  comfffval2  17792  oppchomf  17811  symgga  19537  oppglsm  19772  dfrhm2  20618  cnfldsub  21616  cnflddiv  21618  mat0op  22644  mattpos1  22681  mdetunilem7  22843  madufval  22862  maducoeval2  22865  madugsum  22868  matunitlindflem1  22904  mp2pm2mplem5  23038  mp2pm2mp  23039  leordtval  23441  xpstopnlem1  24038  divcn  25099  oprpiece1res1  25182  oprpiece1res2  25183  ehl1eudis  25651  ehl2eudis  25653  cxpcn  26985  cnnvm  31166  issply  34074  mdetpmtr2  34337  madjusmdetlem1  34340  cnre2csqima  34424  mndpluscn  34439  raddcn  34442  icorempo  38108  mendplusgfval  44025  hoidmv1le  47425  hspdifhsp  47447  vonn0ioo  47518  vonn0icc  47519  dflinc2  49343  cofuoppf  50079  dfswapf2  50190  diag1a  50234  funcsetc1o  50426