Theorem mpoeq3ia 7528

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  ⊤wtru 1538   ∈ wcel 2108   ∈ cmpo 7450

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-oprab 7452  df-mpo 7453

This theorem is referenced by:  mpodifsnif  7565  mposnif  7566  oprab2co  8138  cnfcomlem  9768  cnfcom2  9771  dfioo2  13510  elovmpowrd  14606  sadcom  16509  comfffval2  17759  oppchomf  17780  symgga  19449  oppglsm  19684  dfrhm2  20500  cnfldsub  21433  cnflddiv  21436  cnflddivOLD  21437  mat0op  22446  mattpos1  22483  mdetunilem7  22645  madufval  22664  maducoeval2  22667  madugsum  22670  mp2pm2mplem5  22837  mp2pm2mp  22838  leordtval  23242  xpstopnlem1  23838  divcnOLD  24909  divcn  24911  oprpiece1res1  25001  oprpiece1res2  25002  ehl1eudis  25473  ehl2eudis  25475  cxpcn  26805  cxpcnOLD  26806  cnnvm  30714  mdetpmtr2  33770  madjusmdetlem1  33773  cnre2csqima  33857  mndpluscn  33872  raddcn  33875  icorempo  37317  matunitlindflem1  37576  mendplusgfval  43142  hoidmv1le  46515  hspdifhsp  46537  vonn0ioo  46608  vonn0icc  46609  dflinc2  48139