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

Metamath Proof Explorer

Theorem vexwt

Description: A standard theorem of predicate calculus ( stdpc4 ) expressed using class abstractions. Closed form of vexw . (Contributed by BJ, 14-Jun-2019)

Ref Expression
Assertion vexwt ⊢ ∀ x φ → y ∈ x | φ

Proof

Step Hyp Ref Expression
1 stdpc4 ⊢ ∀ x φ → y x φ
2 df-clab ⊢ y ∈ x | φ ↔ y x φ
3 1 2 sylibr ⊢ ∀ x φ → y ∈ x | φ