Theorem abbi 2795

Description: Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2799, 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.

Step	Hyp	Ref	Expression
1		spsbbi 2074	. . 3 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
2		df-clab 2709	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-clab 2709	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
4	1, 2, 3	3bitr4g 314	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ 𝜓}))
5	4	eqrdv 2728	1 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  [wsb 2065   ∈ wcel 2109  {cab 2708

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 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722

This theorem is referenced by:  abbidv  2796  abbii  2797  abbid  2798  eqab  2867  sbcbi2  3815  iuneq12df  4985  axrep6g  5248  iotabi  6480  uniabio  6481  iotaval  6485  iotanul  6492  iuneq12daf  32492  bj-abv  36901  bj-cleq  36957  abbi1sn  42218  iotain  44413