Theorem mpoeq3ia 7289

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543  ⊤wtru 1544   ∈ wcel 2110   ∈ cmpo 7215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-12 2175  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2071  df-clab 2715  df-cleq 2729  df-oprab 7217  df-mpo 7218

This theorem is referenced by:  mpodifsnif  7325  mposnif  7326  oprab2co  7865  cnfcomlem  9314  cnfcom2  9317  dfioo2  13038  elovmpowrd  14113  sadcom  16022  comfffval2  17204  oppchomf  17224  symgga  18799  oppglsm  19031  dfrhm2  19737  cnfldsub  20391  cnflddiv  20393  mat0op  21316  mattpos1  21353  mdetunilem7  21515  madufval  21534  maducoeval2  21537  madugsum  21540  mp2pm2mplem5  21707  mp2pm2mp  21708  leordtval  22110  xpstopnlem1  22706  divcn  23765  oprpiece1res1  23848  oprpiece1res2  23849  ehl1eudis  24317  ehl2eudis  24319  cxpcn  25631  cnnvm  28763  mdetpmtr2  31488  madjusmdetlem1  31491  cnre2csqima  31575  mndpluscn  31590  raddcn  31593  icorempo  35259  matunitlindflem1  35510  mendplusgfval  40713  hoidmv1le  43807  hspdifhsp  43829  vonn0ioo  43900  vonn0icc  43901  dflinc2  45424