Theorem cnvss 4998

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 4398	. . . 4 |- ( y A x <-> <. y , x >. e. A )
3		df-br 4398	. . . 4 |- ( y B x <-> <. y , x >. e. B )
4	1, 2, 3	3imtr4g 272	. . 3 |- ( A C_ B -> ( y A x -> y B x ) )
5	4	ssopab2dv 4721	. 2 |- ( A C_ B -> { <. x , y >. | y A x } C_ { <. x , y >. | y B x } )
6		df-cnv 4833	. 2 |- `' A = { <. x , y >. | y A x }
7		df-cnv 4833	. 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 1844   C_ wss 3416   <.cop 3980   class class class wbr 4397   {copab 4454   `'ccnv 4824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-in 3423  df-ss 3430  df-br 4398  df-opab 4456  df-cnv 4833

This theorem is referenced by:  cnveq  4999  rnss  5054  relcnvtr  5345  funss  5589  funres11  5639  funcnvres  5640  foimacnv  5818  funcnvuni  6739  tposss  6961  vdwnnlem1  14724  structcnvcnv  14854  catcoppccl  15713  cnvps  16168  tsrdir  16194  gsumzresOLD  17244  gsumzaddOLD  17263  gsum2dOLD  17323  dprdfaddOLD  17389  tsmsresOLD  20939  ustneism  21020  metustsymOLD  21358  metustsym  21359  metustOLD  21364  metust  21365  pi1xfrcnv  21851  eulerpartlemmf  28833  cnvtrrel  35662  relexpaddss  35710