Theorem bj-abex

Description: Two ways of stating that the extension of a formula is a set. (Contributed by BJ, 18-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-abex	⊢ ( { 𝑥 ∣ 𝜑 } ∈ V ↔ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		isset	⊢ ( { 𝑥 ∣ 𝜑 } ∈ V ↔ ∃ 𝑦 𝑦 = { 𝑥 ∣ 𝜑 } )
2		eqabb	⊢ ( 𝑦 = { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )
3	2	exbii	⊢ ( ∃ 𝑦 𝑦 = { 𝑥 ∣ 𝜑 } ↔ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )
4	1 3	bitri	⊢ ( { 𝑥 ∣ 𝜑 } ∈ V ↔ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )