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

Metamath Proof Explorer

Theorem brrpssg

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

Ref Expression
Assertion brrpssg ⊢ B ∈ V → A [⊂] B ↔ A ⊂ B

Proof

Step Hyp Ref Expression
1 elex ⊢ B ∈ V → B ∈ V
2 relrpss ⊢ Rel ⁡ [⊂]
3 2 brrelex1i ⊢ A [⊂] B → A ∈ V
4 1 3 anim12i ⊢ B ∈ V ∧ A [⊂] B → B ∈ V ∧ A ∈ V
5 1 adantr ⊢ B ∈ V ∧ A ⊂ B → B ∈ V
6 pssss ⊢ A ⊂ B → A ⊆ B
7 ssexg ⊢ A ⊆ B ∧ B ∈ V → A ∈ V
8 6 1 7 syl2anr ⊢ B ∈ V ∧ A ⊂ B → A ∈ V
9 5 8 jca ⊢ B ∈ V ∧ A ⊂ B → B ∈ V ∧ A ∈ V
10 psseq1 ⊢ x = A → x ⊂ y ↔ A ⊂ y
11 psseq2 ⊢ y = B → A ⊂ y ↔ A ⊂ B
12 df-rpss ⊢ [⊂] = x y | x ⊂ y
13 10 11 12 brabg ⊢ A ∈ V ∧ B ∈ V → A [⊂] B ↔ A ⊂ B
14 13 ancoms ⊢ B ∈ V ∧ A ∈ V → A [⊂] B ↔ A ⊂ B
15 4 9 14 pm5.21nd ⊢ B ∈ V → A [⊂] B ↔ A ⊂ B