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.

Step	Hyp	Ref	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 )
4	1, 2, 3	3imtr4g 278	. . 3 |- ( A C_ B -> ( y A x -> y B x ) )
5	4	ssopab2dv 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 }
8	5, 6, 7	3sstr4g 3485	1 |- ( A C_ B -> `' A C_ `' B )

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