Theorem mpt2eq3ia 6877

Description: An equality inference for the maps to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

Ref	Expression
mpt2eq3ia.1	⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)

Assertion

Ref	Expression
mpt2eq3ia	⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

Proof of Theorem mpt2eq3ia

Step	Hyp	Ref	Expression
1		mpt2eq3ia.1	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
2	1	3adant1 1124	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷)
3	2	mpt2eq3dva 6876	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷))
4	3	trud 1634	1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1624  ⊤wtru 1625   ∈ wcel 2131   ↦ cmpt2 6807

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-oprab 6809  df-mpt2 6810

This theorem is referenced by:  mpt2difsnif  6910  mpt2snif  6911  oprab2co  7422  cnfcomlem  8761  cnfcom2  8764  dfioo2  12459  elovmpt2wrd  13526  sadcom  15379  comfffval2  16554  oppchomf  16573  symgga  18018  oppglsm  18249  dfrhm2  18911  cnfldsub  19968  cnflddiv  19970  mat0op  20419  mattpos1  20456  mdetunilem7  20618  madufval  20637  maducoeval2  20640  madugsum  20643  mp2pm2mplem5  20809  mp2pm2mp  20810  leordtval  21211  xpstopnlem1  21806  divcn  22864  oprpiece1res1  22943  oprpiece1res2  22944  cxpcn  24677  cnnvm  27838  mdetpmtr2  30191  madjusmdetlem1  30194  cnre2csqima  30258  mndpluscn  30273  raddcn  30276  icorempt2  33502  matunitlindflem1  33710  mendplusgfval  38249  hoidmv1le  41306  hspdifhsp  41328  vonn0ioo  41399  vonn0icc  41400  dflinc2  42701