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

Theorem cnvss 4870
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 3187 . . . 4  |-  ( A 
C_  B  ->  ( <. y ,  x >.  e.  A  ->  <. y ,  x >.  e.  B
) )
2 df-br 4040 . . . 4  |-  ( y A x  <->  <. y ,  x >.  e.  A
)
3 df-br 4040 . . . 4  |-  ( y B x  <->  <. y ,  x >.  e.  B
)
41, 2, 33imtr4g 261 . . 3  |-  ( A 
C_  B  ->  (
y A x  -> 
y B x ) )
54ssopab2dv 4309 . 2  |-  ( A 
C_  B  ->  { <. x ,  y >.  |  y A x }  C_  {
<. x ,  y >.  |  y B x } )
6 df-cnv 4713 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
7 df-cnv 4713 . 2  |-  `' B  =  { <. x ,  y
>.  |  y B x }
85, 6, 73sstr4g 3232 1  |-  ( A 
C_  B  ->  `' A  C_  `' B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    C_ wss 3165   <.cop 3656   class class class wbr 4039   {copab 4092   `'ccnv 4704
This theorem is referenced by:  cnveq  4871  rnss  4923  relcnvtr  5208  funss  5289  funcnvuni  5333  funres11  5336  funcnvres  5337  foimacnv  5506  tposss  6251  vdwnnlem1  13058  structcnvcnv  13175  catcoppccl  13956  cnvps  14337  tsrdir  14376  gsumzres  15210  gsumzadd  15220  gsum2d  15239  dprdfadd  15271  tsmsres  17842  pi1xfrcnv  18571  tdeglem4  19462  twsymr  25181  dualalg  25885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179  df-br 4040  df-opab 4094  df-cnv 4713
  Copyright terms: Public domain W3C validator