Theorem intexab

Description: The intersection of a nonempty class abstraction exists. (Contributed by NM, 21-Oct-2003)

	Ref	Expression
Assertion	intexab	⊢ ( ∃ 𝑥 𝜑 ↔ ∩ { 𝑥 ∣ 𝜑 } ∈ V )

Proof

Step	Hyp	Ref	Expression
1		abn0	⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 𝜑 )
2		intex	⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ ∩ { 𝑥 ∣ 𝜑 } ∈ V )
3	1 2	bitr3i	⊢ ( ∃ 𝑥 𝜑 ↔ ∩ { 𝑥 ∣ 𝜑 } ∈ V )