Metamath Proof Explorer


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 ( 𝑁𝑉 → { 𝑥 ∈ { 𝑁 } ∣ 𝜓 } = { 𝑥𝑉 ∣ ( 𝑥 = 𝑁𝜓 ) } )