Theorem absnsb

Description: If the class abstraction { x | ph } associated with the wff ph is a singleton, the wff is true for the singleton element. (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	absnsb	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		abid	⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
2		velsn	⊢ ( 𝑥 ∈ { 𝑦 } ↔ 𝑥 = 𝑦 )
3	1 2	bibi12i	⊢ ( ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑦 } ) ↔ ( 𝜑 ↔ 𝑥 = 𝑦 ) )
4		biimpr	⊢ ( ( 𝜑 ↔ 𝑥 = 𝑦 ) → ( 𝑥 = 𝑦 → 𝜑 ) )
5	3 4	sylbi	⊢ ( ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑦 } ) → ( 𝑥 = 𝑦 → 𝜑 ) )
6	5	alimi	⊢ ( ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑦 } ) → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
7		nfab1	⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
8		nfcv	⊢ Ⅎ 𝑥 { 𝑦 }
9	7 8	cleqf	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ ∀ 𝑥 ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑥 ∈ { 𝑦 } ) )
10		sb6	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
11	6 9 10	3imtr4i	⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑦 } → [ 𝑦 / 𝑥 ] 𝜑 )