Metamath Proof Explorer

Theorem brssr

Description: The subset relation and subclass relationship ( df-ss ) are the same, that is, ( AS B <-> A C B ) when B is a set. (Contributed by Peter Mazsa, 31-Jul-2019)

Ref Expression
Assertion brssr ⊢ B ∈ V → A S B ↔ A ⊆ B

Proof

Step Hyp Ref Expression
1 relssr ⊢ Rel ⁡ S
2 1 brrelex1i ⊢ A S B → A ∈ V
3 2 adantl ⊢ B ∈ V ∧ A S B → A ∈ V
4 simpl ⊢ B ∈ V ∧ A S B → B ∈ V
5 3 4 jca ⊢ B ∈ V ∧ A S B → A ∈ V ∧ B ∈ V
6 ssexg ⊢ A ⊆ B ∧ B ∈ V → A ∈ V
7 simpr ⊢ A ⊆ B ∧ B ∈ V → B ∈ V
8 6 7 jca ⊢ A ⊆ B ∧ B ∈ V → A ∈ V ∧ B ∈ V
9 8 ancoms ⊢ B ∈ V ∧ A ⊆ B → A ∈ V ∧ B ∈ V
10 sseq1 ⊢ x = A → x ⊆ y ↔ A ⊆ y
11 sseq2 ⊢ y = B → A ⊆ y ↔ A ⊆ B
12 df-ssr ⊢ S = x y | x ⊆ y
13 10 11 12 brabg ⊢ A ∈ V ∧ B ∈ V → A S B ↔ A ⊆ B
14 5 9 13 pm5.21nd ⊢ B ∈ V → A S B ↔ A ⊆ B