Theorem mpteq12dva 5196

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2142, ax-12 2178. (Revised by SN, 11-Nov-2024.)

Hypotheses

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

Assertion

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

Distinct variable group:   𝜑,𝑥

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

Proof of Theorem mpteq12dva

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpteq12dva.2	. . . . . 6 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐷)
2	1	eqeq2d 2741	. . . . 5 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑦 = 𝐷))
3	2	pm5.32da 579	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷)))
4		mpteq12dv.1	. . . . . 6 ⊢ (𝜑 → 𝐴 = 𝐶)
5	4	eleq2d 2815	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐶))
6	5	anbi1d 631	. . . 4 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐷) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)))
7	3, 6	bitrd 279	. . 3 ⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)))
8	7	opabbidv 5176	. 2 ⊢ (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)})
9		df-mpt 5192	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
10		df-mpt 5192	. 2 ⊢ (𝑥 ∈ 𝐶 ↦ 𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐶 ∧ 𝑦 = 𝐷)}
11	8, 9, 10	3eqtr4g 2790	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐶 ↦ 𝐷))

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5172   ↦ cmpt 5191

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-opab 5173  df-mpt 5192

This theorem is referenced by:  mpteq12dv  5197  mpteq2dva  5203  pfxmpt  14650  reps  14742  repswccat  14758  cidpropd  17678  monpropd  17706  fucpropd  17949  curfpropd  18201  hofpropd  18235  yonffthlem  18250  ofco2  22345  pmatcollpw3fi1lem1  22680  rrxnm  25298  ushgredgedg  29163  ushgredgedgloop  29165  cshw1s2  32889  gsumpart  33004  gsumhashmul  33008  gsumwrd2dccat  33014  cycpm2tr  33083  sgnsv  33124  extdg1id  33668  ofcfval  34095  ccatmulgnn0dir  34540  signstf0  34566  curunc  37603  cncfiooicc  45899  dvcosax  45931  fourierdlem74  46185  fourierdlem75  46186  fourierdlem93  46204  smfsupxr  46821  smflimsuplem8  46832  lmdpropd  49650  cmdpropd  49651