Metamath Proof Explorer

Theorem brrpss

Description: The proper subset relation on sets is the same as class proper subsethood. (Contributed by Stefan O'Rear, 2-Nov-2014)

Ref Expression
Hypothesis brrpss.a 
|- B e. _V
Assertion brrpss 
|- ( A [C.] B <-> A C. B )

Proof

Step Hyp Ref Expression
1 brrpss.a 
 |-  B e. _V
2 brrpssg 
 |-  ( B e. _V -> ( A [C.] B <-> A C. B ) )
3 1 2 ax-mp 
 |-  ( A [C.] B <-> A C. B )