Theorem eqabcbw

Description: Version of eqabcb using implicit substitution, which requires fewer axioms. (Contributed by TM, 24-Jan-2026)

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

Proof

Step	Hyp	Ref	Expression
1		eqabbw.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2	1	eqabbw	⊢ ( 𝐴 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝜓 ) )
3		eqcom	⊢ ( { 𝑥 ∣ 𝜑 } = 𝐴 ↔ 𝐴 = { 𝑥 ∣ 𝜑 } )
4		bicom	⊢ ( ( 𝜓 ↔ 𝑦 ∈ 𝐴 ) ↔ ( 𝑦 ∈ 𝐴 ↔ 𝜓 ) )
5	4	albii	⊢ ( ∀ 𝑦 ( 𝜓 ↔ 𝑦 ∈ 𝐴 ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝜓 ) )
6	2 3 5	3bitr4i	⊢ ( { 𝑥 ∣ 𝜑 } = 𝐴 ↔ ∀ 𝑦 ( 𝜓 ↔ 𝑦 ∈ 𝐴 ) )