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

Theorem cnvss 4854
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 3174 . . . 4  |-  ( A 
C_  B  ->  ( <. y ,  x >.  e.  A  ->  <. y ,  x >.  e.  B
) )
2 df-br 4024 . . . 4  |-  ( y A x  <->  <. y ,  x >.  e.  A
)
3 df-br 4024 . . . 4  |-  ( y B x  <->  <. y ,  x >.  e.  B
)
41, 2, 33imtr4g 261 . . 3  |-  ( A 
C_  B  ->  (
y A x  -> 
y B x ) )
54ssopab2dv 4293 . 2  |-  ( A 
C_  B  ->  { <. x ,  y >.  |  y A x }  C_  {
<. x ,  y >.  |  y B x } )
6 df-cnv 4697 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
7 df-cnv 4697 . 2  |-  `' B  =  { <. x ,  y
>.  |  y B x }
85, 6, 73sstr4g 3219 1  |-  ( A 
C_  B  ->  `' A  C_  `' B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1684    C_ wss 3152   <.cop 3643   class class class wbr 4023   {copab 4076   `'ccnv 4688
This theorem is referenced by:  cnveq  4855  rnss  4907  relcnvtr  5192  funss  5273  funcnvuni  5317  funres11  5320  funcnvres  5321  foimacnv  5490  tposss  6235  vdwnnlem1  13042  structcnvcnv  13159  catcoppccl  13940  cnvps  14321  tsrdir  14360  gsumzres  15194  gsumzadd  15204  gsum2d  15223  dprdfadd  15255  tsmsres  17826  pi1xfrcnv  18555  tdeglem4  19446  twsymr  25078  dualalg  25782
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-cnv 4697
  Copyright terms: Public domain W3C validator