Theorem mpoeq3ia 7090

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1522  ⊤wtru 1523   ∈ wcel 2081   ∈ cmpo 7018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-oprab 7020  df-mpo 7021

This theorem is referenced by:  mpodifsnif  7123  mposnif  7124  oprab2co  7648  cnfcomlem  9008  cnfcom2  9011  dfioo2  12688  elovmpowrd  13756  sadcom  15645  comfffval2  16800  oppchomf  16819  symgga  18265  oppglsm  18497  dfrhm2  19159  cnfldsub  20255  cnflddiv  20257  mat0op  20712  mattpos1  20749  mdetunilem7  20911  madufval  20930  maducoeval2  20933  madugsum  20936  mp2pm2mplem5  21102  mp2pm2mp  21103  leordtval  21505  xpstopnlem1  22101  divcn  23159  oprpiece1res1  23238  oprpiece1res2  23239  ehl1eudis  23706  ehl2eudis  23708  cxpcn  25007  cnnvm  28150  mdetpmtr2  30704  madjusmdetlem1  30707  cnre2csqima  30771  mndpluscn  30786  raddcn  30789  icorempo  34163  matunitlindflem1  34419  mendplusgfval  39270  hoidmv1le  42418  hspdifhsp  42440  vonn0ioo  42511  vonn0icc  42512  dflinc2  43945