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		sb8v	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )
5	2 3 4	3bitr4i	⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑥 𝜑 )