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 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )