Theorem mpoeq3ia 7353

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  ⊤wtru 1540   ∈ wcel 2106   ∈ cmpo 7277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-oprab 7279  df-mpo 7280

This theorem is referenced by:  mpodifsnif  7389  mposnif  7390  oprab2co  7937  cnfcomlem  9457  cnfcom2  9460  dfioo2  13182  elovmpowrd  14261  sadcom  16170  comfffval2  17410  oppchomf  17431  symgga  19015  oppglsm  19247  dfrhm2  19961  cnfldsub  20626  cnflddiv  20628  mat0op  21568  mattpos1  21605  mdetunilem7  21767  madufval  21786  maducoeval2  21789  madugsum  21792  mp2pm2mplem5  21959  mp2pm2mp  21960  leordtval  22364  xpstopnlem1  22960  divcn  24031  oprpiece1res1  24114  oprpiece1res2  24115  ehl1eudis  24584  ehl2eudis  24586  cxpcn  25898  cnnvm  29044  mdetpmtr2  31774  madjusmdetlem1  31777  cnre2csqima  31861  mndpluscn  31876  raddcn  31879  icorempo  35522  matunitlindflem1  35773  mendplusgfval  41010  hoidmv1le  44132  hspdifhsp  44154  vonn0ioo  44225  vonn0icc  44226  dflinc2  45751