Metamath Proof Explorer


Theorem ssintab

Description: Subclass of the intersection of a class abstraction. (Contributed by NM, 31-Jul-2006) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion ssintab A x | φ x φ A x

Proof

Step Hyp Ref Expression
1 ssint A x | φ y x | φ A y
2 sseq2 y = x A y A x
3 2 ralab2 y x | φ A y x φ A x
4 1 3 bitri A x | φ x φ A x