Theorem mpoeq3ia 7331

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-oprab 7259  df-mpo 7260

This theorem is referenced by:  mpodifsnif  7367  mposnif  7368  oprab2co  7908  cnfcomlem  9387  cnfcom2  9390  dfioo2  13111  elovmpowrd  14189  sadcom  16098  comfffval2  17327  oppchomf  17348  symgga  18930  oppglsm  19162  dfrhm2  19876  cnfldsub  20538  cnflddiv  20540  mat0op  21476  mattpos1  21513  mdetunilem7  21675  madufval  21694  maducoeval2  21697  madugsum  21700  mp2pm2mplem5  21867  mp2pm2mp  21868  leordtval  22272  xpstopnlem1  22868  divcn  23937  oprpiece1res1  24020  oprpiece1res2  24021  ehl1eudis  24489  ehl2eudis  24491  cxpcn  25803  cnnvm  28945  mdetpmtr2  31676  madjusmdetlem1  31679  cnre2csqima  31763  mndpluscn  31778  raddcn  31781  icorempo  35449  matunitlindflem1  35700  mendplusgfval  40926  hoidmv1le  44022  hspdifhsp  44044  vonn0ioo  44115  vonn0icc  44116  dflinc2  45639