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

Theorem mpteq12dva 5237
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017.) Remove dependency on ax-10 2139, ax-12 2175. (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 2746 . . . . 5 ((𝜑𝑥𝐴) → (𝑦 = 𝐵𝑦 = 𝐷))
32pm5.32da 579 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐴𝑦 = 𝐷)))
4 mpteq12dv.1 . . . . . 6 (𝜑𝐴 = 𝐶)
54eleq2d 2825 . . . . 5 (𝜑 → (𝑥𝐴𝑥𝐶))
65anbi1d 631 . . . 4 (𝜑 → ((𝑥𝐴𝑦 = 𝐷) ↔ (𝑥𝐶𝑦 = 𝐷)))
73, 6bitrd 279 . . 3 (𝜑 → ((𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐶𝑦 = 𝐷)))
87opabbidv 5214 . 2 (𝜑 → {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)})
9 df-mpt 5232 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
10 df-mpt 5232 . 2 (𝑥𝐶𝐷) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐶𝑦 = 𝐷)}
118, 9, 103eqtr4g 2800 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐶𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1537  wcel 2106  {copab 5210  cmpt 5231
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-opab 5211  df-mpt 5232
This theorem is referenced by:  mpteq12dv  5239  mpteq2dva  5248  pfxmpt  14713  reps  14805  repswccat  14821  cidpropd  17755  monpropd  17785  fucpropd  18034  curfpropd  18290  hofpropd  18324  yonffthlem  18339  ofco2  22473  pmatcollpw3fi1lem1  22808  rrxnm  25439  ushgredgedg  29261  ushgredgedgloop  29263  cshw1s2  32930  gsumpart  33043  gsumhashmul  33047  gsumwrd2dccat  33053  cycpm2tr  33122  sgnsv  33163  extdg1id  33691  ofcfval  34079  ccatmulgnn0dir  34536  signstf0  34562  curunc  37589  cncfiooicc  45850  dvcosax  45882  fourierdlem74  46136  fourierdlem75  46137  fourierdlem93  46155  smfsupxr  46772  smflimsuplem8  46783
  Copyright terms: Public domain W3C validator