Theorem euabsn2w

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

	Ref	Expression
Hypotheses	absnw.y	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
	euabsn2w.z	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜃 ) )
Assertion	euabsn2w	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		absnw.y	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
2		euabsn2w.z	⊢ ( 𝑥 = 𝑧 → ( 𝜑 ↔ 𝜃 ) )
3	2 1	eu6w	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
4	2	absnw	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
5	4	exbii	⊢ ( ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑦 ) )
6	3 5	bitr4i	⊢ ( ∃! 𝑥 𝜑 ↔ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )