Theorem cnvss 5856

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3902   class class class wbr 5107  {copab 5171  ^◡ccnv 5658

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ss 3919  df-br 5108  df-opab 5172  df-cnv 5667

This theorem is used by:  cnveq  5857  rnss  5927  relcnvtrg  6267  relcnvtrgOLD  6268  predrelss  6339  funss  6556  funres11  6614  funcnvres  6615  foimacnv  6839  funcnvuni  7932  tposss  8228  vdwnnlem1  17091  structcnvcnv  17249  catcoppccl  18210  cnvps  18670  tsrdir  18696  ustneism  24451  metustsym  24782  metust  24785  pi1xfrcnv  25286  eulerpartlemmf  34873  relcnveq3  39062  elrelscnveq3  39362  disjss  39566  cnvssb  44413  trclubgNEW  44445  clrellem  44449  clcnvlem  44450  cnvrcl0  44452  cnvtrcl0  44453  cnvtrrel  44497  relexpaddss  44545