Theorem cnvss 5726

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

Syntax hints:   → wi 4   ⊆ wss 3853   class class class wbr 5039  {copab 5101  ^◡ccnv 5535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870  df-br 5040  df-opab 5102  df-cnv 5544

This theorem is referenced by:  cnveq  5727  rnss  5793  relcnvtrg  6110  funss  6377  funres11  6435  funcnvres  6436  foimacnv  6656  funcnvuni  7687  tposss  7947  vdwnnlem1  16511  structcnvcnv  16680  catcoppccl  17577  catcoppcclOLD  17578  cnvps  18038  tsrdir  18064  ustneism  23075  metustsym  23407  metust  23410  pi1xfrcnv  23908  eulerpartlemmf  32008  relcnveq3  36142  elrelscnveq3  36295  disjss  36528  cnvssb  40811  trclubgNEW  40843  clrellem  40847  clcnvlem  40848  cnvrcl0  40850  cnvtrcl0  40851  cnvtrrel  40896  relexpaddss  40944