Theorem cnvss

Description: Subset theorem for converse. (Contributed by NM, 22-Mar-1998) (Proof shortened by Kyle Wyonch, 27-Apr-2021)

	Ref	Expression
Assertion	cnvss	⊢ ( 𝐴 ⊆ 𝐵 → ◡ 𝐴 ⊆ ◡ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ssbr	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑦 𝐴 𝑥 → 𝑦 𝐵 𝑥 ) )
2	1	ssopab2dv	⊢ ( 𝐴 ⊆ 𝐵 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝐴 𝑥 } ⊆ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝐵 𝑥 } )
3		df-cnv	⊢ ◡ 𝐴 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝐴 𝑥 }
4		df-cnv	⊢ ◡ 𝐵 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 𝐵 𝑥 }
5	2 3 4	3sstr4g	⊢ ( 𝐴 ⊆ 𝐵 → ◡ 𝐴 ⊆ ◡ 𝐵 )