Theorem cnvss 5847

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   class class class wbr 5103  {copab 5167  ^◡ccnv 5647

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ss 3916  df-br 5104  df-opab 5168  df-cnv 5656

This theorem is used by:  cnveq  5848  rnss  5918  relcnvtrg  6258  relcnvtrgOLD  6259  predrelss  6330  funss  6547  funres11  6606  funcnvres  6607  foimacnv  6831  funcnvuni  7928  tposss  8223  vdwnnlem1  17120  structcnvcnv  17278  catcoppccl  18239  cnvps  18699  tsrdir  18725  ustneism  24490  metustsym  24821  metust  24824  pi1xfrcnv  25325  eulerpartlemmf  34927  relcnveq3  39173  elrelscnveq3  39473  disjss  39677  cnvssb  44524  trclubgNEW  44556  clrellem  44560  clcnvlem  44561  cnvrcl0  44563  cnvtrcl0  44564  cnvtrrel  44608  relexpaddss  44656