Metamath Proof Explorer


Theorem ssint

Description: Subclass of a class intersection. Theorem 5.11(viii) of Monk1 p. 52 and its converse. (Contributed by NM, 14-Oct-1999)

Ref Expression
Assertion ssint A B x B A x

Proof

Step Hyp Ref Expression
1 dfss3 A B y A y B
2 vex y V
3 2 elint2 y B x B y x
4 3 ralbii y A y B y A x B y x
5 ralcom y A x B y x x B y A y x
6 dfss3 A x y A y x
7 6 ralbii x B A x x B y A y x
8 5 7 bitr4i y A x B y x x B A x
9 1 4 8 3bitri A B x B A x