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

Metamath Proof Explorer

Theorem vjust

Description: Justification theorem for df-v . (Contributed by Rodolfo Medina, 27-Apr-2010)

Ref Expression
Assertion vjust { 𝑥 ∣ 𝑥 = 𝑥 } = { 𝑦 ∣ 𝑦 = 𝑦 }

Proof

Step Hyp Ref Expression
1 equid ⊢ 𝑥 = 𝑥
2 1 vexw ⊢ 𝑧 ∈ { 𝑥 ∣ 𝑥 = 𝑥 }
3 equid ⊢ 𝑦 = 𝑦
4 3 vexw ⊢ 𝑧 ∈ { 𝑦 ∣ 𝑦 = 𝑦 }
5 2 4 2th ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝑥 = 𝑥 } ↔ 𝑧 ∈ { 𝑦 ∣ 𝑦 = 𝑦 } )
6 5 eqriv ⊢ { 𝑥 ∣ 𝑥 = 𝑥 } = { 𝑦 ∣ 𝑦 = 𝑦 }