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

Theorem cnvss 4998
Description: Subset theorem for converse. (Contributed by NM, 22-Mar-1998.)
Assertion
Ref Expression
cnvss  |-  ( A 
C_  B  ->  `' A  C_  `' B )

Proof of Theorem cnvss
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssel 3438 . . . 4  |-  ( A 
C_  B  ->  ( <. y ,  x >.  e.  A  ->  <. y ,  x >.  e.  B
) )
2 df-br 4398 . . . 4  |-  ( y A x  <->  <. y ,  x >.  e.  A
)
3 df-br 4398 . . . 4  |-  ( y B x  <->  <. y ,  x >.  e.  B
)
41, 2, 33imtr4g 272 . . 3  |-  ( A 
C_  B  ->  (
y A x  -> 
y B x ) )
54ssopab2dv 4721 . 2  |-  ( A 
C_  B  ->  { <. x ,  y >.  |  y A x }  C_  {
<. x ,  y >.  |  y B x } )
6 df-cnv 4833 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
7 df-cnv 4833 . 2  |-  `' B  =  { <. x ,  y
>.  |  y B x }
85, 6, 73sstr4g 3485 1  |-  ( A 
C_  B  ->  `' A  C_  `' B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1844    C_ wss 3416   <.cop 3980   class class class wbr 4397   {copab 4454   `'ccnv 4824
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-in 3423  df-ss 3430  df-br 4398  df-opab 4456  df-cnv 4833
This theorem is referenced by:  cnveq  4999  rnss  5054  relcnvtr  5345  funss  5589  funres11  5639  funcnvres  5640  foimacnv  5818  funcnvuni  6739  tposss  6961  vdwnnlem1  14724  structcnvcnv  14854  catcoppccl  15713  cnvps  16168  tsrdir  16194  gsumzresOLD  17244  gsumzaddOLD  17263  gsum2dOLD  17323  dprdfaddOLD  17389  tsmsresOLD  20939  ustneism  21020  metustsymOLD  21358  metustsym  21359  metustOLD  21364  metust  21365  pi1xfrcnv  21851  eulerpartlemmf  28833  cnvtrrel  35662  relexpaddss  35710
  Copyright terms: Public domain W3C validator