Theorem mpoeq3ia 7474

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560  ⊤wtru 1561   ∈ wcel 2142   ∈ cmpo 7398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-3an 1100  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-oprab 7400  df-mpo 7401

This theorem is referenced by:  mpodifsnif  7511  mposnif  7512  oprab2co  8076  cnfcomlem  9654  cnfcom2  9657  dfioo2  13454  elovmpowrd  14571  sadcom  16497  comfffval2  17733  oppchomf  17752  symgga  19447  oppglsm  19682  dfrhm2  20523  cnfldsub  21452  cnflddiv  21454  mat0op  22479  mattpos1  22516  mdetunilem7  22678  madufval  22697  maducoeval2  22700  madugsum  22703  mp2pm2mplem5  22870  mp2pm2mp  22871  leordtval  23273  xpstopnlem1  23869  divcn  24930  oprpiece1res1  25013  oprpiece1res2  25014  ehl1eudis  25482  ehl2eudis  25484  cxpcn  26810  cnnvm  30885  issply  33858  mdetpmtr2  34121  madjusmdetlem1  34124  cnre2csqima  34208  mndpluscn  34223  raddcn  34226  icorempo  37845  matunitlindflem1  38115  mendplusgfval  43758  hoidmv1le  47168  hspdifhsp  47190  vonn0ioo  47261  vonn0icc  47262  dflinc2  49032  cofuoppf  49771  dfswapf2  49882  diag1a  49926  funcsetc1o  50118