Theorem cnvss 5822

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

Syntax hints:   → wi 4   ⊆ wss 3902   class class class wbr 5099  {copab 5161  ^◡ccnv 5624

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 3919  df-br 5100  df-opab 5162  df-cnv 5633

This theorem is referenced by:  cnveq  5823  rnss  5889  relcnvtrg  6226  predrelss  6296  funss  6512  funres11  6570  funcnvres  6571  foimacnv  6792  funcnvuni  7877  tposss  8172  vdwnnlem1  16928  structcnvcnv  17085  catcoppccl  18046  cnvps  18506  tsrdir  18532  ustneism  24173  metustsym  24504  metust  24507  pi1xfrcnv  25018  eulerpartlemmf  34545  relcnveq3  38541  elrelscnveq3  38841  disjss  39045  cnvssb  43905  trclubgNEW  43937  clrellem  43941  clcnvlem  43942  cnvrcl0  43944  cnvtrcl0  43945  cnvtrrel  43989  relexpaddss  44037