Theorem cnvss 5590

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

Syntax hints:   → wi 4   ⊆ wss 3828   class class class wbr 4927  {copab 4989  ^◡ccnv 5403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2747

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-in 3835  df-ss 3842  df-br 4928  df-opab 4990  df-cnv 5412

This theorem is referenced by:  cnveq  5591  rnss  5649  relcnvtr  5956  funss  6205  funres11  6262  funcnvres  6263  foimacnv  6459  funcnvuni  7449  tposss  7693  vdwnnlem1  16181  structcnvcnv  16347  catcoppccl  17220  cnvps  17674  tsrdir  17700  ustneism  22529  metustsym  22862  metust  22865  pi1xfrcnv  23358  eulerpartlemmf  31269  relcnveq3  35000  elrelscnveq3  35154  disjss  35387  cnvssb  39286  trclubgNEW  39319  clrellem  39323  clcnvlem  39324  cnvrcl0  39326  cnvtrcl0  39327  cnvtrrel  39356  relexpaddss  39404