Metamath Proof Explorer


Theorem abvALT

Description: Alternate proof of abv , shorter but using more axioms. (Contributed by BJ, 19-Mar-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion abvALT ( { 𝑥𝜑 } = V ↔ ∀ 𝑥 𝜑 )

Proof

Step Hyp Ref Expression
1 df-clab ( 𝑦 ∈ { 𝑥𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
2 1 albii ( ∀ 𝑦 𝑦 ∈ { 𝑥𝜑 } ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
3 eqv ( { 𝑥𝜑 } = V ↔ ∀ 𝑦 𝑦 ∈ { 𝑥𝜑 } )
4 nfv 𝑦 𝜑
5 4 sb8v ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
6 2 3 5 3bitr4i ( { 𝑥𝜑 } = V ↔ ∀ 𝑥 𝜑 )