Theorem bj-vjust

Description: Justification theorem for dfv2 if it were the definition. See also vjust . (Contributed by BJ, 30-Nov-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-vjust	⊢ { 𝑥 ∣ ⊤ } = { 𝑦 ∣ ⊤ }

Proof

Step	Hyp	Ref	Expression
1		vextru	⊢ 𝑧 ∈ { 𝑥 ∣ ⊤ }
2		vextru	⊢ 𝑧 ∈ { 𝑦 ∣ ⊤ }
3	1 2	2th	⊢ ( 𝑧 ∈ { 𝑥 ∣ ⊤ } ↔ 𝑧 ∈ { 𝑦 ∣ ⊤ } )
4	3	eqriv	⊢ { 𝑥 ∣ ⊤ } = { 𝑦 ∣ ⊤ }