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

Theorem mpteq12dva 5238
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2129, ax-12 2166. (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 2736 . . . . 5 ((𝜑𝑥𝐴) → (𝑦 = 𝐵𝑦 = 𝐷))
32pm5.32da 577 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐴𝑦 = 𝐷)))
4 mpteq12dv.1 . . . . . 6 (𝜑𝐴 = 𝐶)
54eleq2d 2811 . . . . 5 (𝜑 → (𝑥𝐴𝑥𝐶))
65anbi1d 629 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐶𝑦 = 𝐷)))
73, 6bitrd 278 . . 3 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐶𝑦 = 𝐷)))
87opabbidv 5215 . 2 (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)})
9 df-mpt 5233 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
10 df-mpt 5233 . 2 (𝑥𝐶𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)}
118, 9, 103eqtr4g 2790 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wcel 2098  {copab 5211  cmpt 5232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-opab 5212  df-mpt 5233
This theorem is referenced by:  mpteq12dv  5240  mpteq2dva  5249  pfxmpt  14664  reps  14756  repswccat  14772  cidpropd  17693  monpropd  17723  fucpropd  17972  curfpropd  18228  hofpropd  18262  yonffthlem  18277  ofco2  22397  pmatcollpw3fi1lem1  22732  rrxnm  25363  ushgredgedg  29114  ushgredgedgloop  29116  cshw1s2  32770  gsumpart  32859  gsumhashmul  32860  cycpm2tr  32932  sgnsv  32973  extdg1id  33486  ofcfval  33848  ccatmulgnn0dir  34305  signstf0  34331  curunc  37206  cncfiooicc  45420  dvcosax  45452  fourierdlem74  45706  fourierdlem75  45707  fourierdlem93  45725  smfsupxr  46342  smflimsuplem8  46353
  Copyright terms: Public domain W3C validator