Theorem cnvss 5819

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

Assertion

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

Proof of Theorem cnvss

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

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

Syntax hints:   → wi 4   ⊆ wss 3890   class class class wbr 5086  {copab 5148  ^◡ccnv 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ss 3907  df-br 5087  df-opab 5149  df-cnv 5630

This theorem is referenced by:  cnveq  5820  rnss  5886  relcnvtrg  6223  predrelss  6293  funss  6509  funres11  6567  funcnvres  6568  foimacnv  6789  funcnvuni  7874  tposss  8168  vdwnnlem1  16955  structcnvcnv  17112  catcoppccl  18073  cnvps  18533  tsrdir  18559  ustneism  24198  metustsym  24529  metust  24532  pi1xfrcnv  25033  eulerpartlemmf  34540  relcnveq3  38659  elrelscnveq3  38959  disjss  39163  cnvssb  44028  trclubgNEW  44060  clrellem  44064  clcnvlem  44065  cnvrcl0  44067  cnvtrcl0  44068  cnvtrrel  44112  relexpaddss  44160