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  7933  tposss  8229  vdwnnlem1  17093  structcnvcnv  17251  catcoppccl  18212  cnvps  18672  tsrdir  18698  ustneism  24456  metustsym  24787  metust  24790  pi1xfrcnv  25291  eulerpartlemmf  34894  relcnveq3  39083  elrelscnveq3  39383  disjss  39587  cnvssb  44434  trclubgNEW  44466  clrellem  44470  clcnvlem  44471  cnvrcl0  44473  cnvtrcl0  44474  cnvtrrel  44518  relexpaddss  44566