Theorem rabsneq

Description: Equality of class abstractions restricted to a singleton. (Contributed by AV, 17-May-2025)

	Ref	Expression
Assertion	rabsneq	⊢ ( 𝑁 ∈ 𝑉 → { 𝑥 ∈ { 𝑁 } ∣ 𝜓 } = { 𝑥 ∈ 𝑉 ∣ ( 𝑥 = 𝑁 ∧ 𝜓 ) } )

Proof

Step	Hyp	Ref	Expression
1		velsn	⊢ ( 𝑥 ∈ { 𝑁 } ↔ 𝑥 = 𝑁 )
2		eleq1a	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑥 = 𝑁 → 𝑥 ∈ 𝑉 ) )
3	2	pm4.71rd	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑥 = 𝑁 ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑥 = 𝑁 ) ) )
4	1 3	bitrid	⊢ ( 𝑁 ∈ 𝑉 → ( 𝑥 ∈ { 𝑁 } ↔ ( 𝑥 ∈ 𝑉 ∧ 𝑥 = 𝑁 ) ) )
5	4	anbi1d	⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑥 ∈ { 𝑁 } ∧ 𝜓 ) ↔ ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 = 𝑁 ) ∧ 𝜓 ) ) )
6		anass	⊢ ( ( ( 𝑥 ∈ 𝑉 ∧ 𝑥 = 𝑁 ) ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝑥 = 𝑁 ∧ 𝜓 ) ) )
7	5 6	bitrdi	⊢ ( 𝑁 ∈ 𝑉 → ( ( 𝑥 ∈ { 𝑁 } ∧ 𝜓 ) ↔ ( 𝑥 ∈ 𝑉 ∧ ( 𝑥 = 𝑁 ∧ 𝜓 ) ) ) )
8	7	abbidv	⊢ ( 𝑁 ∈ 𝑉 → { 𝑥 ∣ ( 𝑥 ∈ { 𝑁 } ∧ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ ( 𝑥 = 𝑁 ∧ 𝜓 ) ) } )
9		df-rab	⊢ { 𝑥 ∈ { 𝑁 } ∣ 𝜓 } = { 𝑥 ∣ ( 𝑥 ∈ { 𝑁 } ∧ 𝜓 ) }
10		df-rab	⊢ { 𝑥 ∈ 𝑉 ∣ ( 𝑥 = 𝑁 ∧ 𝜓 ) } = { 𝑥 ∣ ( 𝑥 ∈ 𝑉 ∧ ( 𝑥 = 𝑁 ∧ 𝜓 ) ) }
11	8 9 10	3eqtr4g	⊢ ( 𝑁 ∈ 𝑉 → { 𝑥 ∈ { 𝑁 } ∣ 𝜓 } = { 𝑥 ∈ 𝑉 ∣ ( 𝑥 = 𝑁 ∧ 𝜓 ) } )