This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V
Assertion brrpss ⊢ A [⊂] B ↔ A ⊂ B

Proof

Step Hyp Ref Expression
1 brrpss.a ⊢ B ∈ V
2 brrpssg ⊢ B ∈ V → A [⊂] B ↔ A ⊂ B
3 1 2 ax-mp ⊢ A [⊂] B ↔ A ⊂ B