Theorem mpoeq3ia 7436

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  ⊤wtru 1542   ∈ wcel 2113   ∈ cmpo 7360

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-oprab 7362  df-mpo 7363

This theorem is referenced by:  mpodifsnif  7473  mposnif  7474  oprab2co  8039  cnfcomlem  9608  cnfcom2  9611  dfioo2  13366  elovmpowrd  14481  sadcom  16390  comfffval2  17624  oppchomf  17643  symgga  19336  oppglsm  19571  dfrhm2  20410  cnfldsub  21352  cnflddiv  21355  cnflddivOLD  21356  mat0op  22363  mattpos1  22400  mdetunilem7  22562  madufval  22581  maducoeval2  22584  madugsum  22587  mp2pm2mplem5  22754  mp2pm2mp  22755  leordtval  23157  xpstopnlem1  23753  divcnOLD  24813  divcn  24815  oprpiece1res1  24905  oprpiece1res2  24906  ehl1eudis  25376  ehl2eudis  25378  cxpcn  26710  cxpcnOLD  26711  cnnvm  30757  issply  33719  mdetpmtr2  33981  madjusmdetlem1  33984  cnre2csqima  34068  mndpluscn  34083  raddcn  34086  icorempo  37556  matunitlindflem1  37817  mendplusgfval  43433  hoidmv1le  46848  hspdifhsp  46870  vonn0ioo  46941  vonn0icc  46942  dflinc2  48666  cofuoppf  49405  dfswapf2  49516  diag1a  49560  funcsetc1o  49752