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

Theorem abbi 2805
Description: Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2809, 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 2071 . . 3 (∀𝑥(𝜑𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
2 df-clab 2713 . . 3 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-clab 2713 . . 3 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
41, 2, 33bitr4g 314 . 2 (∀𝑥(𝜑𝜓) → (𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥𝜓}))
54eqrdv 2733 1 (∀𝑥(𝜑𝜓) → {𝑥𝜑} = {𝑥𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1535   = wceq 1537  [wsb 2062  wcel 2106  {cab 2712
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-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
This theorem is referenced by:  abbidv  2806  abbii  2807  abbid  2808  eqab  2878  sbcbi2  3854  iuneq12df  5023  axrep6g  5296  iotabi  6529  uniabio  6530  iotaval  6534  iotanul  6541  iuneq12daf  32577  bj-abv  36889  bj-cleq  36945  abbi1sn  42241  iotain  44413
  Copyright terms: Public domain W3C validator