Theorem mpteq12dva 5114

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.)

Hypotheses

Ref	Expression
mpteq12dv.1	⊢ (𝜑 → 𝐴 = 𝐶)
mpteq12dva.2	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)

Assertion

Ref	Expression
mpteq12dva	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)   𝐷(𝑥)

Proof of Theorem mpteq12dva

Step	Hyp	Ref	Expression
1		mpteq12dv.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
2	1	alrimiv 1928	. 2 ⊢ (𝜑 → ∀𝑥 𝐴 = 𝐶)
3		mpteq12dva.2	. . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
4	3	ralrimiva 3149	. 2 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 = 𝐷)
5		mpteq12f 5113	. 2 ⊢ ((∀𝑥 𝐴 = 𝐶 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐷) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))
6	2, 4, 5	syl2anc 587	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536   = wceq 1538   ∈ wcel 2111  ∀wral 3106   ↦ cmpt 5110

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-opab 5093  df-mpt 5111

This theorem is referenced by:  mpteq12dvOLD  5116  pfxmpt  14031  reps  14123  repswccat  14139  cidpropd  16972  monpropd  16999  fucpropd  17239  curfpropd  17475  hofpropd  17509  yonffthlem  17524  ofco2  21056  pmatcollpw3fi1lem1  21391  rrxnm  23995  ushgredgedg  27019  ushgredgedgloop  27021  cshw1s2  30660  gsumpart  30740  gsumhashmul  30741  cycpm2tr  30811  sgnsv  30852  extdg1id  31141  ofcfval  31467  ccatmulgnn0dir  31922  signstf0  31948  curunc  35039  cncfiooicc  42536  dvcosax  42568  fourierdlem74  42822  fourierdlem75  42823  fourierdlem93  42841  smfsupxr  43447  smflimsuplem8  43458