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

Theorem abbi 2796
Description: Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2800, proved from fewer axioms, and hence is independently named. (Contributed by BJ and WL and SN, 20-Aug-2023.)
Assertion
Ref Expression
abbi (∀𝑥(𝜑𝜓) → {𝑥𝜑} = {𝑥𝜓})

Proof of Theorem abbi
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 spsbbi 2069 . . 3 (∀𝑥(𝜑𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
2 df-clab 2706 . . 3 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-clab 2706 . . 3 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
41, 2, 33bitr4g 314 . 2 (∀𝑥(𝜑𝜓) → (𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥𝜓}))
54eqrdv 2726 1 (∀𝑥(𝜑𝜓) → {𝑥𝜑} = {𝑥𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wal 1532   = wceq 1534  [wsb 2060  wcel 2099  {cab 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2699
This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720
This theorem is referenced by:  abbidv  2797  abbii  2798  abbid  2799  eqab  2868  sbcbi2  3837  iuneq12df  5017  axrep6g  5287  iotabi  6508  uniabio  6509  iotaval  6513  iotanul  6520  iuneq12daf  32340  bj-abv  36378  bj-cleq  36435  abbi1sn  41705  iotain  43848
  Copyright terms: Public domain W3C validator