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

Theorem cnvss 5165
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 3483 . . . 4  |-  ( A 
C_  B  ->  ( <. y ,  x >.  e.  A  ->  <. y ,  x >.  e.  B
) )
2 df-br 4438 . . . 4  |-  ( y A x  <->  <. y ,  x >.  e.  A
)
3 df-br 4438 . . . 4  |-  ( y B x  <->  <. y ,  x >.  e.  B
)
41, 2, 33imtr4g 270 . . 3  |-  ( A 
C_  B  ->  (
y A x  -> 
y B x ) )
54ssopab2dv 4766 . 2  |-  ( A 
C_  B  ->  { <. x ,  y >.  |  y A x }  C_  {
<. x ,  y >.  |  y B x } )
6 df-cnv 4997 . 2  |-  `' A  =  { <. x ,  y
>.  |  y A x }
7 df-cnv 4997 . 2  |-  `' B  =  { <. x ,  y
>.  |  y B x }
85, 6, 73sstr4g 3530 1  |-  ( A 
C_  B  ->  `' A  C_  `' B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1804    C_ wss 3461   <.cop 4020   class class class wbr 4437   {copab 4494   `'ccnv 4988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-in 3468  df-ss 3475  df-br 4438  df-opab 4496  df-cnv 4997
This theorem is referenced by:  cnveq  5166  rnss  5221  relcnvtr  5517  funss  5596  funres11  5646  funcnvres  5647  foimacnv  5823  funcnvuni  6738  tposss  6958  vdwnnlem1  14495  structcnvcnv  14625  catcoppccl  15414  cnvps  15821  tsrdir  15847  gsumzresOLD  16897  gsumzaddOLD  16916  gsum2dOLD  16979  dprdfaddOLD  17046  tsmsresOLD  20623  ustneism  20704  metustsymOLD  21042  metustsym  21043  metustOLD  21048  metust  21049  pi1xfrcnv  21535  eulerpartlemmf  28292  cnvtrrel  37610
  Copyright terms: Public domain W3C validator