Theorem bj-clex

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

	Ref	Expression
Hypothesis	bj-clex.1	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝜑 )
Assertion	bj-clex	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-clex.1	⊢ ( 𝑥 ∈ 𝐴 ↔ 𝜑 )
2		isset	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑦 𝑦 = 𝐴 )
3		dfcleq	⊢ ( 𝑦 = 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴 ) )
4	1	bibi2i	⊢ ( ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴 ) ↔ ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )
5	4	albii	⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴 ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )
6	3 5	bitri	⊢ ( 𝑦 = 𝐴 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )
7	6	exbii	⊢ ( ∃ 𝑦 𝑦 = 𝐴 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )
8	2 7	bitri	⊢ ( 𝐴 ∈ V ↔ ∃ 𝑦 ∀ 𝑥 ( 𝑥 ∈ 𝑦 ↔ 𝜑 ) )