Theorem mpoeq3ia 7485

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

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

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 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-oprab 7409  df-mpo 7410

This theorem is referenced by:  mpodifsnif  7522  mposnif  7523  oprab2co  8096  cnfcomlem  9713  cnfcom2  9716  dfioo2  13467  elovmpowrd  14576  sadcom  16482  comfffval2  17713  oppchomf  17732  symgga  19388  oppglsm  19623  dfrhm2  20434  cnfldsub  21360  cnflddiv  21363  cnflddivOLD  21364  mat0op  22357  mattpos1  22394  mdetunilem7  22556  madufval  22575  maducoeval2  22578  madugsum  22581  mp2pm2mplem5  22748  mp2pm2mp  22749  leordtval  23151  xpstopnlem1  23747  divcnOLD  24808  divcn  24810  oprpiece1res1  24900  oprpiece1res2  24901  ehl1eudis  25372  ehl2eudis  25374  cxpcn  26706  cxpcnOLD  26707  cnnvm  30663  mdetpmtr2  33855  madjusmdetlem1  33858  cnre2csqima  33942  mndpluscn  33957  raddcn  33960  icorempo  37369  matunitlindflem1  37640  mendplusgfval  43205  hoidmv1le  46623  hspdifhsp  46645  vonn0ioo  46716  vonn0icc  46717  dflinc2  48386  dfswapf2  49178  diag1a  49216  funcsetc1o  49382