Theorem brcnvssr

Description: The converse of a subset relation swaps arguments. (Contributed by Peter Mazsa, 1-Aug-2019)

	Ref	Expression
Assertion	brcnvssr	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ◡ S 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		relssr	⊢ Rel S
2	1	relbrcnv	⊢ ( 𝐴 ◡ S 𝐵 ↔ 𝐵 S 𝐴 )
3		brssr	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐵 S 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
4	2 3	bitrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ◡ S 𝐵 ↔ 𝐵 ⊆ 𝐴 ) )