Theorem cnvss 5820

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 5141	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑦𝐴𝑥 → 𝑦𝐵𝑥))
2	1	ssopab2dv 5498	. 2 ⊢ (𝐴 ⊆ 𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
3		df-cnv 5631	. 2 ⊢ ◡𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
4		df-cnv 5631	. 2 ⊢ ◡𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
5	2, 3, 4	3sstr4g 3986	1 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)

Syntax hints:   → wi 4   ⊆ wss 3900   class class class wbr 5097  {copab 5159  ^◡ccnv 5622

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-sb 2069  df-clab 2714  df-cleq 2727  df-clel 2810  df-ss 3917  df-br 5098  df-opab 5160  df-cnv 5631

This theorem is referenced by:  cnveq  5821  rnss  5887  relcnvtrg  6224  predrelss  6294  funss  6510  funres11  6568  funcnvres  6569  foimacnv  6790  funcnvuni  7874  tposss  8169  vdwnnlem1  16925  structcnvcnv  17082  catcoppccl  18043  cnvps  18503  tsrdir  18529  ustneism  24170  metustsym  24501  metust  24504  pi1xfrcnv  25015  eulerpartlemmf  34511  relcnveq3  38497  elrelscnveq3  38797  disjss  39001  cnvssb  43864  trclubgNEW  43896  clrellem  43900  clcnvlem  43901  cnvrcl0  43903  cnvtrcl0  43904  cnvtrrel  43948  relexpaddss  43996