MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq12dva Structured version   Visualization version   GIF version

Theorem mpteq12dva 5231
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2141, ax-12 2177. (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.
StepHypRef Expression
1 mpteq12dva.2 . . . . . 6 ((𝜑𝑥𝐴) → 𝐵 = 𝐷)
21eqeq2d 2748 . . . . 5 ((𝜑𝑥𝐴) → (𝑦 = 𝐵𝑦 = 𝐷))
32pm5.32da 579 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐴𝑦 = 𝐷)))
4 mpteq12dv.1 . . . . . 6 (𝜑𝐴 = 𝐶)
54eleq2d 2827 . . . . 5 (𝜑 → (𝑥𝐴𝑥𝐶))
65anbi1d 631 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐶𝑦 = 𝐷)))
73, 6bitrd 279 . . 3 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐶𝑦 = 𝐷)))
87opabbidv 5209 . 2 (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)})
9 df-mpt 5226 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
10 df-mpt 5226 . 2 (𝑥𝐶𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)}
118, 9, 103eqtr4g 2802 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  wcel 2108  {copab 5205  cmpt 5225
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 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-opab 5206  df-mpt 5226
This theorem is referenced by:  mpteq12dv  5233  mpteq2dva  5242  pfxmpt  14716  reps  14808  repswccat  14824  cidpropd  17753  monpropd  17781  fucpropd  18025  curfpropd  18278  hofpropd  18312  yonffthlem  18327  ofco2  22457  pmatcollpw3fi1lem1  22792  rrxnm  25425  ushgredgedg  29246  ushgredgedgloop  29248  cshw1s2  32945  gsumpart  33060  gsumhashmul  33064  gsumwrd2dccat  33070  cycpm2tr  33139  sgnsv  33180  extdg1id  33716  ofcfval  34099  ccatmulgnn0dir  34557  signstf0  34583  curunc  37609  cncfiooicc  45909  dvcosax  45941  fourierdlem74  46195  fourierdlem75  46196  fourierdlem93  46214  smfsupxr  46831  smflimsuplem8  46842
  Copyright terms: Public domain W3C validator