Theorem cnvss 5825

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

Syntax hints:   → wi 4   ⊆ wss 3890   class class class wbr 5086  {copab 5148  ^◡ccnv 5627

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 3907  df-br 5087  df-opab 5149  df-cnv 5636

This theorem is referenced by:  cnveq  5826  rnss  5892  relcnvtrg  6229  predrelss  6299  funss  6515  funres11  6573  funcnvres  6574  foimacnv  6795  funcnvuni  7880  tposss  8174  vdwnnlem1  16963  structcnvcnv  17120  catcoppccl  18081  cnvps  18541  tsrdir  18567  ustneism  24205  metustsym  24536  metust  24539  pi1xfrcnv  25040  eulerpartlemmf  34541  relcnveq3  38670  elrelscnveq3  38970  disjss  39174  cnvssb  44039  trclubgNEW  44071  clrellem  44075  clcnvlem  44076  cnvrcl0  44078  cnvtrcl0  44079  cnvtrrel  44123  relexpaddss  44171