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

Theorem cnvss 5829
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 5150 . . 3 (𝐴𝐵 → (𝑦𝐴𝑥𝑦𝐵𝑥))
21ssopab2dv 5509 . 2 (𝐴𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
3 df-cnv 5642 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
4 df-cnv 5642 . 2 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
52, 3, 43sstr4g 3990 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3911   class class class wbr 5106  {copab 5168  ccnv 5633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-br 5107  df-opab 5169  df-cnv 5642
This theorem is referenced by:  cnveq  5830  rnss  5895  relcnvtrg  6219  predrelss  6292  funss  6521  funres11  6579  funcnvres  6580  foimacnv  6802  funcnvuni  7869  tposss  8159  vdwnnlem1  16872  structcnvcnv  17030  catcoppccl  18008  catcoppcclOLD  18009  cnvps  18472  tsrdir  18498  ustneism  23591  metustsym  23927  metust  23930  pi1xfrcnv  24436  eulerpartlemmf  33032  relcnveq3  36828  elrelscnveq3  36999  disjss  37239  cnvssb  41946  trclubgNEW  41978  clrellem  41982  clcnvlem  41983  cnvrcl0  41985  cnvtrcl0  41986  cnvtrrel  42030  relexpaddss  42078
  Copyright terms: Public domain W3C validator