Theorem eqabdv

Description: Deduction from a wff to a class abstraction. (Contributed by NM, 9-Jul-1994) Avoid ax-11 . (Revised by Wolf Lammen, 6-May-2023)

	Ref	Expression
Hypothesis	eqabdv.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝜓 ) )
Assertion	eqabdv	⊢ ( 𝜑 → 𝐴 = { 𝑥 ∣ 𝜓 } )

Proof

Step	Hyp	Ref	Expression
1		eqabdv.1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↔ 𝜓 ) )
2	1	sbbidv	⊢ ( 𝜑 → ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝜓 ) )
3		clelsb1	⊢ ( [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 )
4	3	bicomi	⊢ ( 𝑦 ∈ 𝐴 ↔ [ 𝑦 / 𝑥 ] 𝑥 ∈ 𝐴 )
5		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜓 } ↔ [ 𝑦 / 𝑥 ] 𝜓 )
6	2 4 5	3bitr4g	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜓 } ) )
7	6	eqrdv	⊢ ( 𝜑 → 𝐴 = { 𝑥 ∣ 𝜓 } )