Theorem abbi 2799

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

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1537   = wceq 1539  [wsb 2063   ∈ wcel 2107  {cab 2712

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726

This theorem is referenced by:  abbidv  2800  abbii  2801  abbid  2802  eqab  2872  sbcbi2  3829  iuneq12df  4998  axrep6g  5270  iotabi  6507  uniabio  6508  iotaval  6512  iotanul  6519  iuneq12daf  32505  bj-abv  36882  bj-cleq  36938  abbi1sn  42237  iotain  44408