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	⊢ ( ∀ 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } = V )

Proof

Step	Hyp	Ref	Expression
1		ax-5	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
2		vexwt	⊢ ( ∀ 𝑥 𝜑 → 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
3	1 2	alrimih	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
4		eqv	⊢ ( { 𝑥 ∣ 𝜑 } = V ↔ ∀ 𝑦 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
5	3 4	sylibr	⊢ ( ∀ 𝑥 𝜑 → { 𝑥 ∣ 𝜑 } = V )