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	⊢ { 𝑥 ∣ 𝑥 = 𝑥 } = { 𝑦 ∣ 𝑦 = 𝑦 }