Theorem cnvss 5175

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.

Step	Hyp	Ref	Expression
1		ssel 3498	. . . 4 |- ( A C_ B -> ( <. y , x >. e. A -> <. y , x >. e. B ) )
2		df-br 4448	. . . 4 |- ( y A x <-> <. y , x >. e. A )
3		df-br 4448	. . . 4 |- ( y B x <-> <. y , x >. e. B )
4	1, 2, 3	3imtr4g 270	. . 3 |- ( A C_ B -> ( y A x -> y B x ) )
5	4	ssopab2dv 4776	. 2 |- ( A C_ B -> { <. x , y >. | y A x } C_ { <. x , y >. | y B x } )
6		df-cnv 5007	. 2 |- `' A = { <. x , y >. | y A x }
7		df-cnv 5007	. 2 |- `' B = { <. x , y >. | y B x }
8	5, 6, 7	3sstr4g 3545	1 |- ( A C_ B -> `' A C_ `' B )

Syntax hints:   -> wi 4   e. wcel 1767   C_ wss 3476   <.cop 4033   class class class wbr 4447   {copab 4504   `'ccnv 4998

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-in 3483  df-ss 3490  df-br 4448  df-opab 4506  df-cnv 5007

This theorem is referenced by:  cnveq  5176  rnss  5231  relcnvtr  5527  funss  5606  funres11  5656  funcnvres  5657  foimacnv  5833  funcnvuni  6737  tposss  6956  vdwnnlem1  14372  structcnvcnv  14501  catcoppccl  15293  cnvps  15699  tsrdir  15725  gsumzresOLD  16721  gsumzaddOLD  16740  gsum2dOLD  16803  dprdfaddOLD  16869  tsmsresOLD  20408  ustneism  20489  metustsymOLD  20827  metustsym  20828  metustOLD  20833  metust  20834  pi1xfrcnv  21320  eulerpartlemmf  27982  cnvtrrel  36810