Theorem absnw

Description: Replace ax-10 , ax-11 , ax-12 in absn with a substitution hypothesis. (Contributed by SN, 27-May-2025)

	Ref	Expression
Hypothesis	absnw.y	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	absnw	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) )

Proof

Step	Hyp	Ref	Expression
1		absnw.y	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		df-sn	⊢ { 𝑌 } = { 𝑥 ∣ 𝑥 = 𝑌 }
3	2	eqeq2i	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑌 } )
4		eqeq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑌 ↔ 𝑦 = 𝑌 ) )
5	1 4	abbibw	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) )
6	3 5	bitri	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) )