Theorem abbi 2800

Description: Equivalent formulas yield equal class abstractions (closed form). This is the backward implication of abbib 2804, 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 2076	. . 3 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → ([𝑦 / 𝑥]𝜑 ↔ [𝑦 / 𝑥]𝜓))
2		df-clab 2710	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ [𝑦 / 𝑥]𝜑)
3		df-clab 2710	. . 3 ⊢ (𝑦 ∈ {𝑥 ∣ 𝜓} ↔ [𝑦 / 𝑥]𝜓)
4	1, 2, 3	3bitr4g 313	. 2 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → (𝑦 ∈ {𝑥 ∣ 𝜑} ↔ 𝑦 ∈ {𝑥 ∣ 𝜓}))
5	4	eqrdv 2730	1 ⊢ (∀𝑥(𝜑 ↔ 𝜓) → {𝑥 ∣ 𝜑} = {𝑥 ∣ 𝜓})

Syntax hints:   → wi 4   ↔ wb 205  ∀wal 1539   = wceq 1541  [wsb 2067   ∈ wcel 2106  {cab 2709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724

This theorem is referenced by:  abbidv  2801  abbii  2802  abbid  2803  eqab  2872  sbcbi2  3839  iuneq12df  5023  axrep6g  5293  iotabi  6509  uniabio  6510  iotaval  6514  iotanul  6521  iuneq12daf  31826  bj-abv  35878  bj-cleq  35935  abbi1sn  41132  iotain  43264