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

Theorem cnvss 5883
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 5187 . . 3 (𝐴𝐵 → (𝑦𝐴𝑥𝑦𝐵𝑥))
21ssopab2dv 5556 . 2 (𝐴𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
3 df-cnv 5693 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
4 df-cnv 5693 . 2 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
52, 3, 43sstr4g 4037 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3951   class class class wbr 5143  {copab 5205  ccnv 5684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-cnv 5693
This theorem is referenced by:  cnveq  5884  rnss  5950  relcnvtrg  6286  predrelss  6358  funss  6585  funres11  6643  funcnvres  6644  foimacnv  6865  funcnvuni  7954  tposss  8252  vdwnnlem1  17033  structcnvcnv  17190  catcoppccl  18162  cnvps  18623  tsrdir  18649  ustneism  24232  metustsym  24568  metust  24571  pi1xfrcnv  25090  eulerpartlemmf  34377  relcnveq3  38322  elrelscnveq3  38492  disjss  38732  cnvssb  43599  trclubgNEW  43631  clrellem  43635  clcnvlem  43636  cnvrcl0  43638  cnvtrcl0  43639  cnvtrrel  43683  relexpaddss  43731
  Copyright terms: Public domain W3C validator