Theorem mpoeq3ia 7470

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  ⊤wtru 1541   ∈ wcel 2109   ∈ cmpo 7392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-oprab 7394  df-mpo 7395

This theorem is referenced by:  mpodifsnif  7507  mposnif  7508  oprab2co  8079  cnfcomlem  9659  cnfcom2  9662  dfioo2  13418  elovmpowrd  14530  sadcom  16440  comfffval2  17669  oppchomf  17688  symgga  19344  oppglsm  19579  dfrhm2  20390  cnfldsub  21316  cnflddiv  21319  cnflddivOLD  21320  mat0op  22313  mattpos1  22350  mdetunilem7  22512  madufval  22531  maducoeval2  22534  madugsum  22537  mp2pm2mplem5  22704  mp2pm2mp  22705  leordtval  23107  xpstopnlem1  23703  divcnOLD  24764  divcn  24766  oprpiece1res1  24856  oprpiece1res2  24857  ehl1eudis  25327  ehl2eudis  25329  cxpcn  26661  cxpcnOLD  26662  cnnvm  30618  mdetpmtr2  33821  madjusmdetlem1  33824  cnre2csqima  33908  mndpluscn  33923  raddcn  33926  icorempo  37346  matunitlindflem1  37617  mendplusgfval  43177  hoidmv1le  46599  hspdifhsp  46621  vonn0ioo  46692  vonn0icc  46693  dflinc2  48403  cofuoppf  49143  dfswapf2  49254  diag1a  49298  funcsetc1o  49490