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

Theorem cnvss 5510
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 4899 . . 3 (𝐴𝐵 → (𝑦𝐴𝑥𝑦𝐵𝑥))
21ssopab2dv 5212 . 2 (𝐴𝐵 → {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥} ⊆ {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥})
3 df-cnv 5332 . 2 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐴𝑥}
4 df-cnv 5332 . 2 𝐵 = {⟨𝑥, 𝑦⟩ ∣ 𝑦𝐵𝑥}
52, 3, 43sstr4g 3854 1 (𝐴𝐵𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3780   class class class wbr 4855  {copab 4917  ccnv 5323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-in 3787  df-ss 3794  df-br 4856  df-opab 4918  df-cnv 5332
This theorem is referenced by:  cnveq  5511  rnss  5569  relcnvtr  5883  funss  6130  funres11  6187  funcnvres  6188  foimacnv  6380  funcnvuni  7359  tposss  7598  vdwnnlem1  15936  structcnvcnv  16102  catcoppccl  16982  cnvps  17437  tsrdir  17463  ustneism  22261  metustsym  22594  metust  22597  pi1xfrcnv  23090  eulerpartlemmf  30785  relcnveq3  34426  elrelscnveq3  34573  cnvssb  38410  trclubgNEW  38443  clrellem  38447  clcnvlem  38448  cnvrcl0  38450  cnvtrcl0  38451  cnvtrrel  38480  relexpaddss  38528
  Copyright terms: Public domain W3C validator