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 2138, ax-12 2172. (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 2744 . . . . 5 ((𝜑𝑥𝐴) → (𝑦 = 𝐵𝑦 = 𝐷))
32pm5.32da 580 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐴𝑦 = 𝐷)))
4 mpteq12dv.1 . . . . . 6 (𝜑𝐴 = 𝐶)
54eleq2d 2820 . . . . 5 (𝜑 → (𝑥𝐴𝑥𝐶))
65anbi1d 631 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐶𝑦 = 𝐷)))
73, 6bitrd 279 . . 3 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐶𝑦 = 𝐷)))
87opabbidv 5215 . 2 (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)})
9 df-mpt 5233 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
10 df-mpt 5233 . 2 (𝑥𝐶𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)}
118, 9, 103eqtr4g 2798 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  wcel 2107  {copab 5211  cmpt 5232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-opab 5212  df-mpt 5233
This theorem is referenced by:  mpteq12dv  5240  mpteq2dva  5249  pfxmpt  14628  reps  14720  repswccat  14736  cidpropd  17654  monpropd  17684  fucpropd  17930  curfpropd  18186  hofpropd  18220  yonffthlem  18235  ofco2  21953  pmatcollpw3fi1lem1  22288  rrxnm  24908  ushgredgedg  28486  ushgredgedgloop  28488  cshw1s2  32124  gsumpart  32207  gsumhashmul  32208  cycpm2tr  32278  sgnsv  32319  extdg1id  32742  ofcfval  33096  ccatmulgnn0dir  33553  signstf0  33579  curunc  36470  cncfiooicc  44610  dvcosax  44642  fourierdlem74  44896  fourierdlem75  44897  fourierdlem93  44915  smfsupxr  45532  smflimsuplem8  45543
  Copyright terms: Public domain W3C validator