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

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

Proof of Theorem abbi1
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 spsbbi 2050 . . 3 (∀𝑥(𝜑𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
2 df-clab 2775 . . 3 (𝑦 ∈ {𝑥𝜑} ↔ [𝑦 / 𝑥]𝜑)
3 df-clab 2775 . . 3 (𝑦 ∈ {𝑥𝜓} ↔ [𝑦 / 𝑥]𝜓)
41, 2, 33bitr4g 315 . 2 (∀𝑥(𝜑𝜓) → (𝑦 ∈ {𝑥𝜑} ↔ 𝑦 ∈ {𝑥𝜓}))
54eqrdv 2792 1 (∀𝑥(𝜑𝜓) → {𝑥𝜑} = {𝑥𝜓})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207  ∀wal 1520   = wceq 1522  [wsb 2041   ∈ wcel 2080  {cab 2774 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-9 2090  ax-ext 2768 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1763  df-sb 2042  df-clab 2775  df-cleq 2787 This theorem is referenced by:  abbidv  2859  abbii  2860  abbid  2861  iuneq12df  4852  iotabi  6201  uniabio  6202  iotanul  6207  iuneq12daf  29990  bj-cleq  33843  iotain  40300
 Copyright terms: Public domain W3C validator