This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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