Theorem mpoeq3ia 7498

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  ⊤wtru 1571   ∈ wcel 2145   ∈ cmpo 7422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-oprab 7424  df-mpo 7425

This theorem is used by:  mpodifsnif  7535  mposnif  7536  oprab2co  8108  cnfcomlem  9700  cnfcom2  9703  dfioo2  13581  elovmpowrd  14703  sadcom  16633  comfffval2  17875  oppchomf  17894  symgga  19621  oppglsm  19856  dfrhm2  20704  cnfldsub  21706  cnflddiv  21708  mat0op  22734  mattpos1  22771  mdetunilem7  22933  madufval  22952  maducoeval2  22955  madugsum  22958  matunitlindflem1  22994  mp2pm2mplem5  23128  mp2pm2mp  23129  leordtval  23531  xpstopnlem1  24128  divcn  25189  oprpiece1res1  25272  oprpiece1res2  25273  ehl1eudis  25741  ehl2eudis  25743  cxpcn  27073  cnnvm  31284  issply  34193  mdetpmtr2  34456  madjusmdetlem1  34459  cnre2csqima  34543  mndpluscn  34558  raddcn  34561  icorempo  38274  mendplusgfval  44182  hoidmv1le  47603  hspdifhsp  47625  vonn0ioo  47696  vonn0icc  47697  dflinc2  49521  cofuoppf  50257  dfswapf2  50368  diag1a  50412  funcsetc1o  50604