Theorem abbi

Description: Equivalent formulas define equal class abstractions, and conversely. (Contributed by NM, 25-Nov-2013) (Revised by Mario Carneiro, 11-Aug-2016) Remove dependency on ax-8 and df-clel (by avoiding use of cleqh ). (Revised by BJ, 23-Jun-2019)

	Ref	Expression
Assertion	abbi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		dfcleq	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) )
2		nfsab1	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜑 }
3		nfsab1	⊢ Ⅎ 𝑥 𝑦 ∈ { 𝑥 ∣ 𝜓 }
4	2 3	nfbi	⊢ Ⅎ 𝑥 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } )
5		nfv	⊢ Ⅎ 𝑦 ( 𝜑 ↔ 𝜓 )
6		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
7		sbequ12r	⊢ ( 𝑦 = 𝑥 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) )
8	6 7	bitrid	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 ) )
9		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 )
10		sbequ12r	⊢ ( 𝑦 = 𝑥 → ( [ 𝑦 / 𝑥 ] 𝜓 ↔ 𝜓 ) )
11	9 10	bitrid	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ 𝜓 ) )
12	8 11	bibi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ( 𝜑 ↔ 𝜓 ) ) )
13	4 5 12	cbvalv1	⊢ ( ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) ↔ ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) )
14	1 13	bitr2i	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )