Theorem sseq2 3252

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 3235	. . . 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 3235	. . . 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 3243	. 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 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sseq12  3253  sseq2i  3255  sseq2d  3258  sseqtrid  3278  nssne1  3286  sseq0  3538  un00  3543  pweq  3659  ssintab  3950  ssintub  3951  intmin  3953  treq  4198  ssexg  4233  exmidundif  4302  frforeq3  4450  frirrg  4453  iunpw  4583  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  ordtri2or2exmid  4675  ontri2orexmidim  4676  iotaexab  5312  fununi  5405  funcnvuni  5406  feq3  5474  ssimaexg  5717  nnawordex  6740  ereq1  6752  xpider  6818  domeng  6966  ssfiexmid  7106  ssfiexmidt  7108  fisseneq  7170  sbthlemi4  7202  sbthlemi5  7203  nninfninc  7382  acfun  7482  onntri45  7519  ccfunen  7543  fprodssdc  12231  lspf  14485  lspval  14486  basis2  14859  eltg2  14864  clsval  14922  ntrcls0  14942  isnei  14955  neiint  14956  neipsm  14965  opnneissb  14966  opnssneib  14967  innei  14974  icnpimaex  15022  cnptoprest2  15051  neitx  15079  txcnp  15082  blssps  15238  blss  15239  metss  15305  metrest  15317  metcnp3  15322  upgredgpr  16090  wlkvtxiedg  16286  wlkvtxiedgg  16287  wlkres  16320  bdssexg  16620  bj-nntrans  16667  bj-omtrans  16672