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

Theorem cnvss 5029
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 4419 . . . 4  |-  ( y A x  <->  <. y ,  x >.  e.  A
)
3 df-br 4419 . . . 4  |-  ( y B x  <->  <. y ,  x >.  e.  B
)
41, 2, 33imtr4g 278 . . 3  |-  ( A 
C_  B  ->  (
y A x  -> 
y B x ) )
54ssopab2dv 4747 . 2  |-  ( A 
C_  B  ->  { <. x ,  y >.  |  y A x }  C_  {
<. x ,  y >.  |  y B x } )
6 df-cnv 4864 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
7 df-cnv 4864 . 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 1898    C_ wss 3416   <.cop 3986   class class class wbr 4418   {copab 4476   `'ccnv 4855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-in 3423  df-ss 3430  df-br 4419  df-opab 4478  df-cnv 4864
This theorem is referenced by:  cnveq  5030  rnss  5085  relcnvtr  5378  funss  5623  funres11  5677  funcnvres  5678  foimacnv  5858  funcnvuni  6778  tposss  7005  vdwnnlem1  15000  structcnvcnv  15187  catcoppccl  16058  cnvps  16513  tsrdir  16539  ustneism  21293  metustsym  21625  metust  21628  pi1xfrcnv  22143  eulerpartlemmf  29258  cnvssb  36238  trclubgNEW  36271  clrellem  36275  clcnvlem  36276  cnvrcl0  36278  cnvtrcl0  36279  cnvtrrel  36308  relexpaddss  36356
  Copyright terms: Public domain W3C validator