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.

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

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