Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnvss Structured version   Visualization version   GIF version

Theorem cnvss 5327
 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.
StepHypRef Expression
1 ssbr 4729 . . 3 (𝐴𝐵 → (𝑦𝐴𝑥𝑦𝐵𝑥))
21ssopab2dv 5033 . 2 (𝐴𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
3 df-cnv 5151 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
4 df-cnv 5151 . 2 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
52, 3, 43sstr4g 3679 1 (𝐴𝐵𝐴𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊆ wss 3607   class class class wbr 4685  {copab 4745  ◡ccnv 5142 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621  df-br 4686  df-opab 4746  df-cnv 5151 This theorem is referenced by:  cnveq  5328  rnss  5386  relcnvtr  5693  funss  5945  funres11  6004  funcnvres  6005  foimacnv  6192  funcnvuni  7161  tposss  7398  vdwnnlem1  15746  structcnvcnv  15918  catcoppccl  16805  cnvps  17259  tsrdir  17285  ustneism  22074  metustsym  22407  metust  22410  pi1xfrcnv  22903  eulerpartlemmf  30565  relcnveq3  34233  elrelscnveq3  34381  cnvssb  38209  trclubgNEW  38242  clrellem  38246  clcnvlem  38247  cnvrcl0  38249  cnvtrcl0  38250  cnvtrrel  38279  relexpaddss  38327
 Copyright terms: Public domain W3C validator