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

Metamath Proof Explorer

Theorem bj-abvALT

Description: Alternate version of bj-abv ; shorter but uses ax-8 . (Contributed by BJ, 24-Jul-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-abvALT ⊢ ∀ x φ → x | φ = V

Proof

Step Hyp Ref Expression
1 ax-5 ⊢ ∀ x φ → ∀ y ∀ x φ
2 vexwt ⊢ ∀ x φ → y ∈ x | φ
3 1 2 alrimih ⊢ ∀ x φ → ∀ y y ∈ x | φ
4 eqv ⊢ x | φ = V ↔ ∀ y y ∈ x | φ
5 3 4 sylibr ⊢ ∀ x φ → x | φ = V