Theorem sseq2 3262

Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)

Assertion

Ref	Expression
sseq2	|- ( A = B -> ( C C_ A <-> C C_ B ) )

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 3245	. . . 4 |- ( C C_ A -> ( A C_ B -> C C_ B ) )
2	1	com12 30	. . 3 |- ( A C_ B -> ( C C_ A -> C C_ B ) )
3		sstr2 3245	. . . 4 |- ( C C_ B -> ( B C_ A -> C C_ A ) )
4	3	com12 30	. . 3 |- ( B C_ A -> ( C C_ B -> C C_ A ) )
5	2, 4	anim12i 338	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( ( C C_ A -> C C_ B ) /\ ( C C_ B -> C C_ A ) ) )
6		eqss 3253	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
7		dfbi2 388	. 2 |- ( ( C C_ A <-> C C_ B ) <-> ( ( C C_ A -> C C_ B ) /\ ( C C_ B -> C C_ A ) ) )
8	5, 6, 7	3imtr4i 201	1 |- ( A = B -> ( C C_ A <-> C C_ B ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1398   C_ wss 3211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  sseq12  3263  sseq2i  3265  sseq2d  3268  sseqtrid  3288  nssne1  3296  sseq0  3550  un00  3555  pweq  3672  ssintab  3966  ssintub  3967  intmin  3969  treq  4214  ssexg  4249  exmidundif  4319  frforeq3  4468  frirrg  4471  iunpw  4601  ordtri2orexmid  4645  ontr2exmid  4647  onsucsssucexmid  4649  ordtri2or2exmid  4693  ontri2orexmidim  4694  iotaexab  5331  fununi  5424  funcnvuni  5425  feq3  5493  ssimaexg  5739  nnawordex  6762  ereq1  6774  xpider  6840  domeng  6989  ssfiexmid  7131  ssfiexmidt  7133  fisseneq  7195  sbthlemi4  7230  sbthlemi5  7231  nninfninc  7414  acfun  7514  onntri45  7551  ccfunen  7578  fprodssdc  12276  lspf  14537  lspval  14538  basis2  14913  eltg2  14918  clsval  14976  ntrcls0  14996  isnei  15009  neiint  15010  neipsm  15019  opnneissb  15020  opnssneib  15021  innei  15028  icnpimaex  15076  cnptoprest2  15105  neitx  15133  txcnp  15136  blssps  15292  blss  15293  metss  15359  metrest  15371  metcnp3  15376  upgredgpr  16144  wlkvtxiedg  16340  wlkvtxiedgg  16341  wlkres  16374  bdssexg  16674  bj-nntrans  16721  bj-omtrans  16726