Theorem mpoeq3ia 7445

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

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

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 2708

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 2715  df-cleq 2728  df-oprab 7371  df-mpo 7372

This theorem is referenced by:  mpodifsnif  7482  mposnif  7483  oprab2co  8047  cnfcomlem  9620  cnfcom2  9623  dfioo2  13403  elovmpowrd  14520  sadcom  16432  comfffval2  17667  oppchomf  17686  symgga  19382  oppglsm  19617  dfrhm2  20454  cnfldsub  21380  cnflddiv  21382  mat0op  22384  mattpos1  22421  mdetunilem7  22583  madufval  22602  maducoeval2  22605  madugsum  22608  mp2pm2mplem5  22775  mp2pm2mp  22776  leordtval  23178  xpstopnlem1  23774  divcn  24835  oprpiece1res1  24918  oprpiece1res2  24919  ehl1eudis  25387  ehl2eudis  25389  cxpcn  26709  cnnvm  30753  issply  33705  mdetpmtr2  33968  madjusmdetlem1  33971  cnre2csqima  34055  mndpluscn  34070  raddcn  34073  icorempo  37667  matunitlindflem1  37937  mendplusgfval  43609  hoidmv1le  47022  hspdifhsp  47044  vonn0ioo  47115  vonn0icc  47116  dflinc2  48886  cofuoppf  49625  dfswapf2  49736  diag1a  49780  funcsetc1o  49972