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

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 ( 𝐵 ∈ 𝑉 → ( 𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 relssr ⊢ Rel S
2 1 brrelex1i ⊢ ( 𝐴 S 𝐵 → 𝐴 ∈ V )
3 2 adantl ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 S 𝐵 ) → 𝐴 ∈ V )
4 simpl ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 S 𝐵 ) → 𝐵 ∈ 𝑉 )
5 3 4 jca ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 S 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) )
6 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V )
7 simpr ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
8 6 7 jca ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) )
9 8 ancoms ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) )
10 sseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝑦 ) )
11 sseq2 ⊢ ( 𝑦 = 𝐵 → ( 𝐴 ⊆ 𝑦 ↔ 𝐴 ⊆ 𝐵 ) )
12 df-ssr ⊢ S = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊆ 𝑦 }
13 10 11 12 brabg ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
14 5 9 13 pm5.21nd ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 S 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )