Theorem cnvss 5839

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

Syntax hints:   → wi 4   ⊆ wss 3917   class class class wbr 5110  {copab 5172  ^◡ccnv 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ss 3934  df-br 5111  df-opab 5173  df-cnv 5649

This theorem is referenced by:  cnveq  5840  rnss  5906  relcnvtrg  6242  predrelss  6313  funss  6538  funres11  6596  funcnvres  6597  foimacnv  6820  funcnvuni  7911  tposss  8209  vdwnnlem1  16973  structcnvcnv  17130  catcoppccl  18086  cnvps  18544  tsrdir  18570  ustneism  24118  metustsym  24450  metust  24453  pi1xfrcnv  24964  eulerpartlemmf  34373  relcnveq3  38316  elrelscnveq3  38489  disjss  38730  cnvssb  43582  trclubgNEW  43614  clrellem  43618  clcnvlem  43619  cnvrcl0  43621  cnvtrcl0  43622  cnvtrrel  43666  relexpaddss  43714