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

Theorem abbi 2807
Description: Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2811, 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 2073 . . 3 (∀𝑥(𝜑𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
2 df-clab 2715 . . 3 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-clab 2715 . . 3 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
41, 2, 33bitr4g 314 . 2 (∀𝑥(𝜑𝜓) → (𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥𝜓}))
54eqrdv 2735 1 (∀𝑥(𝜑𝜓) → {𝑥𝜑} = {𝑥𝜓})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wal 1538   = wceq 1540  [wsb 2064  wcel 2108  {cab 2714
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729
This theorem is referenced by:  abbidv  2808  abbii  2809  abbid  2810  eqab  2880  sbcbi2  3848  iuneq12df  5018  axrep6g  5290  iotabi  6527  uniabio  6528  iotaval  6532  iotanul  6539  iuneq12daf  32569  bj-abv  36907  bj-cleq  36963  abbi1sn  42262  iotain  44436
  Copyright terms: Public domain W3C validator