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

Theorem mpteq12dva 5236
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2135, ax-12 2169. (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 2741 . . . . 5 ((𝜑𝑥𝐴) → (𝑦 = 𝐵𝑦 = 𝐷))
32pm5.32da 577 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐴𝑦 = 𝐷)))
4 mpteq12dv.1 . . . . . 6 (𝜑𝐴 = 𝐶)
54eleq2d 2817 . . . . 5 (𝜑 → (𝑥𝐴𝑥𝐶))
65anbi1d 628 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐶𝑦 = 𝐷)))
73, 6bitrd 278 . . 3 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐶𝑦 = 𝐷)))
87opabbidv 5213 . 2 (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)})
9 df-mpt 5231 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
10 df-mpt 5231 . 2 (𝑥𝐶𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)}
118, 9, 103eqtr4g 2795 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1539  wcel 2104  {copab 5209  cmpt 5230
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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-opab 5210  df-mpt 5231
This theorem is referenced by:  mpteq12dv  5238  mpteq2dva  5247  pfxmpt  14632  reps  14724  repswccat  14740  cidpropd  17658  monpropd  17688  fucpropd  17934  curfpropd  18190  hofpropd  18224  yonffthlem  18239  ofco2  22173  pmatcollpw3fi1lem1  22508  rrxnm  25139  ushgredgedg  28753  ushgredgedgloop  28755  cshw1s2  32391  gsumpart  32477  gsumhashmul  32478  cycpm2tr  32548  sgnsv  32589  extdg1id  33030  ofcfval  33394  ccatmulgnn0dir  33851  signstf0  33877  curunc  36773  cncfiooicc  44908  dvcosax  44940  fourierdlem74  45194  fourierdlem75  45195  fourierdlem93  45213  smfsupxr  45830  smflimsuplem8  45841
  Copyright terms: Public domain W3C validator