Theorem mpoeq3ia 7427

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109   ∈ cmpo 7351

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-oprab 7353  df-mpo 7354

This theorem is referenced by:  mpodifsnif  7464  mposnif  7465  oprab2co  8030  cnfcomlem  9595  cnfcom2  9598  dfioo2  13353  elovmpowrd  14465  sadcom  16374  comfffval2  17607  oppchomf  17626  symgga  19286  oppglsm  19521  dfrhm2  20359  cnfldsub  21304  cnflddiv  21307  cnflddivOLD  21308  mat0op  22304  mattpos1  22341  mdetunilem7  22503  madufval  22522  maducoeval2  22525  madugsum  22528  mp2pm2mplem5  22695  mp2pm2mp  22696  leordtval  23098  xpstopnlem1  23694  divcnOLD  24755  divcn  24757  oprpiece1res1  24847  oprpiece1res2  24848  ehl1eudis  25318  ehl2eudis  25320  cxpcn  26652  cxpcnOLD  26653  cnnvm  30626  mdetpmtr2  33797  madjusmdetlem1  33800  cnre2csqima  33884  mndpluscn  33899  raddcn  33902  icorempo  37335  matunitlindflem1  37606  mendplusgfval  43164  hoidmv1le  46585  hspdifhsp  46607  vonn0ioo  46678  vonn0icc  46679  dflinc2  48405  cofuoppf  49145  dfswapf2  49256  diag1a  49300  funcsetc1o  49492