Theorem mpoeq3ia 7489

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  ⊤wtru 1568   ∈ wcel 2149   ∈ cmpo 7413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-oprab 7415  df-mpo 7416

This theorem is referenced by:  mpodifsnif  7526  mposnif  7527  oprab2co  8092  cnfcomlem  9668  cnfcom2  9671  dfioo2  13477  elovmpowrd  14595  sadcom  16521  comfffval2  17757  oppchomf  17776  symgga  19477  oppglsm  19712  dfrhm2  20556  cnfldsub  21519  cnflddiv  21521  mat0op  22545  mattpos1  22582  mdetunilem7  22744  madufval  22763  maducoeval2  22766  madugsum  22769  mp2pm2mplem5  22936  mp2pm2mp  22937  leordtval  23339  xpstopnlem1  23935  divcn  24996  oprpiece1res1  25079  oprpiece1res2  25080  ehl1eudis  25548  ehl2eudis  25550  cxpcn  26876  cnnvm  30975  issply  33896  mdetpmtr2  34159  madjusmdetlem1  34162  cnre2csqima  34246  mndpluscn  34261  raddcn  34264  icorempo  37885  matunitlindflem1  38155  mendplusgfval  43800  hoidmv1le  47200  hspdifhsp  47222  vonn0ioo  47293  vonn0icc  47294  dflinc2  49075  cofuoppf  49813  dfswapf2  49924  diag1a  49968  funcsetc1o  50160