Theorem abeq2w

Description: Version of abeq2 using implicit substitution, which requires fewer axioms. (Contributed by GG and AV, 18-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		abeq2w.1	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		dfcleq	⊢ ( 𝐴 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) )
3		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
4	1	sbievw	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
5	3 4	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜓 )
6	5	bibi2i	⊢ ( ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ( 𝑦 ∈ 𝐴 ↔ 𝜓 ) )
7	6	albii	⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝜓 ) )
8	2 7	bitri	⊢ ( 𝐴 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 ↔ 𝜓 ) )