Metamath Proof Explorer


Theorem intexab

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

Ref Expression
Assertion intexab xφx|φV

Proof

Step Hyp Ref Expression
1 abn0 x|φxφ
2 intex x|φx|φV
3 1 2 bitr3i xφx|φV