Theorem cnvssb

Description: Subclass theorem for converse. (Contributed by RP, 22-Oct-2020)

	Ref	Expression
Assertion	cnvssb	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ◡ 𝐴 ⊆ ◡ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		cnvss	⊢ ( 𝐴 ⊆ 𝐵 → ◡ 𝐴 ⊆ ◡ 𝐵 )
2		cnvss	⊢ ( ◡ 𝐴 ⊆ ◡ 𝐵 → ◡ ◡ 𝐴 ⊆ ◡ ◡ 𝐵 )
3		dfrel2	⊢ ( Rel 𝐴 ↔ ◡ ◡ 𝐴 = 𝐴 )
4	3	biimpi	⊢ ( Rel 𝐴 → ◡ ◡ 𝐴 = 𝐴 )
5	4	eqcomd	⊢ ( Rel 𝐴 → 𝐴 = ◡ ◡ 𝐴 )
6	5	adantr	⊢ ( ( Rel 𝐴 ∧ ◡ ◡ 𝐴 ⊆ ◡ ◡ 𝐵 ) → 𝐴 = ◡ ◡ 𝐴 )
7		id	⊢ ( ◡ ◡ 𝐴 ⊆ ◡ ◡ 𝐵 → ◡ ◡ 𝐴 ⊆ ◡ ◡ 𝐵 )
8		cnvcnvss	⊢ ◡ ◡ 𝐵 ⊆ 𝐵
9	7 8	sstrdi	⊢ ( ◡ ◡ 𝐴 ⊆ ◡ ◡ 𝐵 → ◡ ◡ 𝐴 ⊆ 𝐵 )
10	9	adantl	⊢ ( ( Rel 𝐴 ∧ ◡ ◡ 𝐴 ⊆ ◡ ◡ 𝐵 ) → ◡ ◡ 𝐴 ⊆ 𝐵 )
11	6 10	eqsstrd	⊢ ( ( Rel 𝐴 ∧ ◡ ◡ 𝐴 ⊆ ◡ ◡ 𝐵 ) → 𝐴 ⊆ 𝐵 )
12	11	ex	⊢ ( Rel 𝐴 → ( ◡ ◡ 𝐴 ⊆ ◡ ◡ 𝐵 → 𝐴 ⊆ 𝐵 ) )
13	2 12	syl5	⊢ ( Rel 𝐴 → ( ◡ 𝐴 ⊆ ◡ 𝐵 → 𝐴 ⊆ 𝐵 ) )
14	1 13	impbid2	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ◡ 𝐴 ⊆ ◡ 𝐵 ) )