Theorem cnvss 5870

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

Syntax hints:   → wi 4   ⊆ wss 3947   class class class wbr 5147  {copab 5209  ^◡ccnv 5674

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964  df-br 5148  df-opab 5210  df-cnv 5683

This theorem is referenced by:  cnveq  5871  rnss  5936  relcnvtrg  6262  predrelss  6335  funss  6564  funres11  6622  funcnvres  6623  foimacnv  6847  funcnvuni  7918  tposss  8208  vdwnnlem1  16924  structcnvcnv  17082  catcoppccl  18063  catcoppcclOLD  18064  cnvps  18527  tsrdir  18553  ustneism  23719  metustsym  24055  metust  24058  pi1xfrcnv  24564  eulerpartlemmf  33362  relcnveq3  37178  elrelscnveq3  37349  disjss  37589  cnvssb  42322  trclubgNEW  42354  clrellem  42358  clcnvlem  42359  cnvrcl0  42361  cnvtrcl0  42362  cnvtrrel  42406  relexpaddss  42454