Theorem cnvss 5862

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

Syntax hints:   → wi 4   ⊆ wss 3913   class class class wbr 5114  {copab 5178  ^◡ccnv 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ss 3930  df-br 5115  df-opab 5179  df-cnv 5673

This theorem is referenced by:  cnveq  5863  rnss  5933  relcnvtrg  6272  predrelss  6342  funss  6559  funres11  6617  funcnvres  6618  foimacnv  6842  funcnvuni  7932  tposss  8226  vdwnnlem1  17058  structcnvcnv  17216  catcoppccl  18177  cnvps  18637  tsrdir  18663  ustneism  24364  metustsym  24695  metust  24698  pi1xfrcnv  25199  eulerpartlemmf  34735  relcnveq3  38926  elrelscnveq3  39226  disjss  39430  cnvssb  44264  trclubgNEW  44296  clrellem  44300  clcnvlem  44301  cnvrcl0  44303  cnvtrcl0  44304  cnvtrrel  44348  relexpaddss  44396