Theorem cnvss 5852

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

Syntax hints:   → wi 4   ⊆ wss 3926   class class class wbr 5119  {copab 5181  ^◡ccnv 5653

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ss 3943  df-br 5120  df-opab 5182  df-cnv 5662

This theorem is referenced by:  cnveq  5853  rnss  5919  relcnvtrg  6255  predrelss  6326  funss  6555  funres11  6613  funcnvres  6614  foimacnv  6835  funcnvuni  7928  tposss  8226  vdwnnlem1  17015  structcnvcnv  17172  catcoppccl  18130  cnvps  18588  tsrdir  18614  ustneism  24162  metustsym  24494  metust  24497  pi1xfrcnv  25008  eulerpartlemmf  34407  relcnveq3  38339  elrelscnveq3  38509  disjss  38749  cnvssb  43610  trclubgNEW  43642  clrellem  43646  clcnvlem  43647  cnvrcl0  43649  cnvtrcl0  43650  cnvtrrel  43694  relexpaddss  43742