Theorem cnvss 5886

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

Syntax hints:   → wi 4   ⊆ wss 3963   class class class wbr 5148  {copab 5210  ^◡ccnv 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-ss 3980  df-br 5149  df-opab 5211  df-cnv 5697

This theorem is referenced by:  cnveq  5887  rnss  5953  relcnvtrg  6288  predrelss  6360  funss  6587  funres11  6645  funcnvres  6646  foimacnv  6866  funcnvuni  7955  tposss  8251  vdwnnlem1  17029  structcnvcnv  17187  catcoppccl  18171  catcoppcclOLD  18172  cnvps  18636  tsrdir  18662  ustneism  24248  metustsym  24584  metust  24587  pi1xfrcnv  25104  eulerpartlemmf  34357  relcnveq3  38303  elrelscnveq3  38473  disjss  38713  cnvssb  43576  trclubgNEW  43608  clrellem  43612  clcnvlem  43613  cnvrcl0  43615  cnvtrcl0  43616  cnvtrrel  43660  relexpaddss  43708