Theorem mpoeq3ia 7446

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ⊤wtru 1543   ∈ wcel 2114   ∈ cmpo 7370

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-oprab 7372  df-mpo 7373

This theorem is referenced by:  mpodifsnif  7483  mposnif  7484  oprab2co  8049  cnfcomlem  9620  cnfcom2  9623  dfioo2  13378  elovmpowrd  14493  sadcom  16402  comfffval2  17636  oppchomf  17655  symgga  19351  oppglsm  19586  dfrhm2  20425  cnfldsub  21367  cnflddiv  21370  cnflddivOLD  21371  mat0op  22378  mattpos1  22415  mdetunilem7  22577  madufval  22596  maducoeval2  22599  madugsum  22602  mp2pm2mplem5  22769  mp2pm2mp  22770  leordtval  23172  xpstopnlem1  23768  divcnOLD  24828  divcn  24830  oprpiece1res1  24920  oprpiece1res2  24921  ehl1eudis  25391  ehl2eudis  25393  cxpcn  26725  cxpcnOLD  26726  cnnvm  30774  issply  33742  mdetpmtr2  34006  madjusmdetlem1  34009  cnre2csqima  34093  mndpluscn  34108  raddcn  34111  icorempo  37610  matunitlindflem1  37871  mendplusgfval  43542  hoidmv1le  46956  hspdifhsp  46978  vonn0ioo  47049  vonn0icc  47050  dflinc2  48774  cofuoppf  49513  dfswapf2  49624  diag1a  49668  funcsetc1o  49860