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.

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

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