Theorem abbi 2810

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1535   = wceq 1537  [wsb 2064   ∈ wcel 2108  {cab 2717

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732

This theorem is referenced by:  abbidv  2811  abbii  2812  abbid  2813  eqab  2883  sbcbi2  3867  iuneq12df  5041  axrep6g  5311  iotabi  6539  uniabio  6540  iotaval  6544  iotanul  6551  iuneq12daf  32579  bj-abv  36872  bj-cleq  36928  abbi1sn  42216  iotain  44386