Theorem cnvss 5849

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   class class class wbr 5102  {copab 5166  ^◡ccnv 5649

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3896  df-br 5103  df-opab 5167  df-cnv 5658

This theorem is used by:  cnveq  5850  rnss  5920  cnvssb  6188  relcnvtrg  6268  relcnvtrgOLD  6269  predrelss  6340  funss  6558  funres11  6617  funcnvres  6618  foimacnv  6842  funcnvuni  7944  tposss  8244  vdwnnlem1  17173  structcnvcnv  17331  catcoppccl  18292  cnvps  18752  tsrdir  18778  ustneism  24543  metustsym  24874  metust  24877  pi1xfrcnv  25378  eulerpartlemmf  35007  relcnveq3  39260  elrelscnveq3  39560  disjss  39764  trclubgNEW  44618  clrellem  44622  clcnvlem  44623  cnvrcl0  44625  cnvtrcl0  44626  cnvtrrel  44670  relexpaddss  44718