Theorem mpoeq3ia 7424

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ⊤wtru 1542   ∈ wcel 2111   ∈ cmpo 7348

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 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-oprab 7350  df-mpo 7351

This theorem is referenced by:  mpodifsnif  7461  mposnif  7462  oprab2co  8027  cnfcomlem  9589  cnfcom2  9592  dfioo2  13350  elovmpowrd  14465  sadcom  16374  comfffval2  17607  oppchomf  17626  symgga  19319  oppglsm  19554  dfrhm2  20392  cnfldsub  21334  cnflddiv  21337  cnflddivOLD  21338  mat0op  22334  mattpos1  22371  mdetunilem7  22533  madufval  22552  maducoeval2  22555  madugsum  22558  mp2pm2mplem5  22725  mp2pm2mp  22726  leordtval  23128  xpstopnlem1  23724  divcnOLD  24784  divcn  24786  oprpiece1res1  24876  oprpiece1res2  24877  ehl1eudis  25347  ehl2eudis  25349  cxpcn  26681  cxpcnOLD  26682  cnnvm  30662  issply  33584  mdetpmtr2  33837  madjusmdetlem1  33840  cnre2csqima  33924  mndpluscn  33939  raddcn  33942  icorempo  37395  matunitlindflem1  37666  mendplusgfval  43284  hoidmv1le  46702  hspdifhsp  46724  vonn0ioo  46795  vonn0icc  46796  dflinc2  48521  cofuoppf  49261  dfswapf2  49372  diag1a  49416  funcsetc1o  49608