Metamath Proof Explorer

Theorem ssrabeq

Description: If the restricting class of a restricted class abstraction is a subset of this restricted class abstraction, it is equal to this restricted class abstraction. (Contributed by Alexander van der Vekens, 31-Dec-2017)

Ref Expression
Assertion ssrabeq V x V | φ V = x V | φ


Step Hyp Ref Expression
1 ssrab2 x V | φ V
2 1 biantru V x V | φ V x V | φ x V | φ V
3 eqss V = x V | φ V x V | φ x V | φ V
4 2 3 bitr4i V x V | φ V = x V | φ