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

Theorem cnvss 5180
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 3497 . . . 4
2 df-br 4453 . . . 4
3 df-br 4453 . . . 4
41, 2, 33imtr4g 270 . . 3
54ssopab2dv 4781 . 2
6 df-cnv 5012 . 2
7 df-cnv 5012 . 2
85, 6, 73sstr4g 3544 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  C_wss 3475  <.cop 4035   class class class wbr 4452  {copab 4509  `'ccnv 5003
This theorem is referenced by:  cnveq  5181  rnss  5236  relcnvtr  5532  funss  5611  funres11  5661  funcnvres  5662  foimacnv  5838  funcnvuni  6753  tposss  6975  vdwnnlem1  14513  structcnvcnv  14643  catcoppccl  15435  cnvps  15842  tsrdir  15868  gsumzresOLD  16918  gsumzaddOLD  16937  gsum2dOLD  17000  dprdfaddOLD  17067  tsmsresOLD  20645  ustneism  20726  metustsymOLD  21064  metustsym  21065  metustOLD  21070  metust  21071  pi1xfrcnv  21557  eulerpartlemmf  28314  cnvtrrel  37782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489  df-br 4453  df-opab 4511  df-cnv 5012
  Copyright terms: Public domain W3C validator