Theorem cnvss 5846

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

Syntax hints:   → wi 4   ⊆ wss 3906   class class class wbr 5102  {copab 5164  ^◡ccnv 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-ss 3923  df-br 5103  df-opab 5165  df-cnv 5657

This theorem is referenced by:  cnveq  5847  rnss  5917  relcnvtrg  6256  predrelss  6326  funss  6542  funres11  6600  funcnvres  6601  foimacnv  6826  funcnvuni  7915  tposss  8209  vdwnnlem1  17033  structcnvcnv  17191  catcoppccl  18152  cnvps  18612  tsrdir  18638  ustneism  24286  metustsym  24617  metust  24620  pi1xfrcnv  25121  eulerpartlemmf  34674  relcnveq3  38831  elrelscnveq3  39131  disjss  39335  cnvssb  44167  trclubgNEW  44199  clrellem  44203  clcnvlem  44204  cnvrcl0  44206  cnvtrcl0  44207  cnvtrrel  44251  relexpaddss  44299