Theorem mpoeq3ia 7505

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569  ⊤wtru 1570   ∈ wcel 2146   ∈ cmpo 7429

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-oprab 7431  df-mpo 7432

This theorem is used by:  mpodifsnif  7542  mposnif  7543  oprab2co  8117  cnfcomlem  9710  cnfcom2  9713  dfioo2  13591  elovmpowrd  14713  sadcom  16645  comfffval2  17887  oppchomf  17906  symgga  19633  oppglsm  19868  dfrhm2  20716  cnfldsub  21718  cnflddiv  21720  mat0op  22746  mattpos1  22783  mdetunilem7  22945  madufval  22964  maducoeval2  22967  madugsum  22970  matunitlindflem1  23006  mp2pm2mplem5  23140  mp2pm2mp  23141  leordtval  23543  xpstopnlem1  24140  divcn  25201  oprpiece1res1  25284  oprpiece1res2  25285  ehl1eudis  25753  ehl2eudis  25755  cxpcn  27085  cnnvm  31296  issply  34246  mdetpmtr2  34509  madjusmdetlem1  34512  cnre2csqima  34596  mndpluscn  34611  raddcn  34614  icorempo  38414  mendplusgfval  44323  hoidmv1le  47743  hspdifhsp  47765  vonn0ioo  47836  vonn0icc  47837  dflinc2  49661  cofuoppf  50405  dfswapf2  50522  diag1a  50566  funcsetc1o  50771