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

Theorem cnvss 5175
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 3498 . . . 4  |-  ( A 
C_  B  ->  ( <. y ,  x >.  e.  A  ->  <. y ,  x >.  e.  B
) )
2 df-br 4448 . . . 4  |-  ( y A x  <->  <. y ,  x >.  e.  A
)
3 df-br 4448 . . . 4  |-  ( y B x  <->  <. y ,  x >.  e.  B
)
41, 2, 33imtr4g 270 . . 3  |-  ( A 
C_  B  ->  (
y A x  -> 
y B x ) )
54ssopab2dv 4776 . 2  |-  ( A 
C_  B  ->  { <. x ,  y >.  |  y A x }  C_  {
<. x ,  y >.  |  y B x } )
6 df-cnv 5007 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
7 df-cnv 5007 . 2  |-  `' B  =  { <. x ,  y
>.  |  y B x }
85, 6, 73sstr4g 3545 1  |-  ( A 
C_  B  ->  `' A  C_  `' B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1767    C_ wss 3476   <.cop 4033   class class class wbr 4447   {copab 4504   `'ccnv 4998
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490  df-br 4448  df-opab 4506  df-cnv 5007
This theorem is referenced by:  cnveq  5176  rnss  5231  relcnvtr  5527  funss  5606  funres11  5656  funcnvres  5657  foimacnv  5833  funcnvuni  6737  tposss  6956  vdwnnlem1  14372  structcnvcnv  14501  catcoppccl  15293  cnvps  15699  tsrdir  15725  gsumzresOLD  16721  gsumzaddOLD  16740  gsum2dOLD  16803  dprdfaddOLD  16869  tsmsresOLD  20408  ustneism  20489  metustsymOLD  20827  metustsym  20828  metustOLD  20833  metust  20834  pi1xfrcnv  21320  eulerpartlemmf  27982  cnvtrrel  36810
  Copyright terms: Public domain W3C validator