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

Theorem cnvss 5129
Description: Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
cnvss

Proof of Theorem cnvss
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3464 . . . 4
2 df-br 4410 . . . 4
3 df-br 4410 . . . 4
41, 2, 33imtr4g 270 . . 3
54ssopab2dv 4734 . 2
6 df-cnv 4965 . 2
7 df-cnv 4965 . 2
85, 6, 73sstr4g 3511 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1758  C_wss 3442  <.cop 3999   class class class wbr 4409  {copab 4466  `'ccnv 4956
This theorem is referenced by:  cnveq  5130  rnss  5185  relcnvtr  5476  funss  5555  funres11  5605  funcnvres  5606  foimacnv  5780  funcnvuni  6663  tposss  6880  vdwnnlem1  14214  structcnvcnv  14343  catcoppccl  15135  cnvps  15541  tsrdir  15567  gsumzresOLD  16553  gsumzaddOLD  16572  gsum2dOLD  16633  dprdfaddOLD  16692  tsmsresOLD  20116  ustneism  20197  metustsymOLD  20535  metustsym  20536  metustOLD  20541  metust  20542  pi1xfrcnv  21028  eulerpartlemmf  27214  cnvtrrel  36483
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-in 3449  df-ss 3456  df-br 4410  df-opab 4468  df-cnv 4965
  Copyright terms: Public domain W3C validator