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

Theorem cnvss 5011
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 3349 . . . 4  |-  ( A 
C_  B  ->  ( <. y ,  x >.  e.  A  ->  <. y ,  x >.  e.  B
) )
2 df-br 4292 . . . 4  |-  ( y A x  <->  <. y ,  x >.  e.  A
)
3 df-br 4292 . . . 4  |-  ( y B x  <->  <. y ,  x >.  e.  B
)
41, 2, 33imtr4g 270 . . 3  |-  ( A 
C_  B  ->  (
y A x  -> 
y B x ) )
54ssopab2dv 4616 . 2  |-  ( A 
C_  B  ->  { <. x ,  y >.  |  y A x }  C_  {
<. x ,  y >.  |  y B x } )
6 df-cnv 4847 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
7 df-cnv 4847 . 2  |-  `' B  =  { <. x ,  y
>.  |  y B x }
85, 6, 73sstr4g 3396 1  |-  ( A 
C_  B  ->  `' A  C_  `' B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1756    C_ wss 3327   <.cop 3882   class class class wbr 4291   {copab 4348   `'ccnv 4838
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2567  df-in 3334  df-ss 3341  df-br 4292  df-opab 4350  df-cnv 4847
This theorem is referenced by:  cnveq  5012  rnss  5067  relcnvtr  5356  funss  5435  funres11  5485  funcnvres  5486  foimacnv  5657  funcnvuni  6529  tposss  6745  vdwnnlem1  14055  structcnvcnv  14184  catcoppccl  14975  cnvps  15381  tsrdir  15407  gsumzresOLD  16391  gsumzaddOLD  16410  gsum2dOLD  16463  dprdfaddOLD  16516  tsmsresOLD  19716  ustneism  19797  metustsymOLD  20135  metustsym  20136  metustOLD  20141  metust  20142  pi1xfrcnv  20628  eulerpartlemmf  26757
  Copyright terms: Public domain W3C validator