Theorem sseq2 3266

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 3249	. . . 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 3249	. . . 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 3257	. 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 3214

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  sseq12  3267  sseq2i  3269  sseq2d  3272  sseqtrid  3292  nssne1  3300  sseq0  3554  un00  3559  pweq  3677  ssintab  3971  ssintub  3972  intmin  3974  treq  4219  ssexg  4254  exmidundif  4324  frforeq3  4473  frirrg  4476  iunpw  4606  ordtri2orexmid  4650  ontr2exmid  4652  onsucsssucexmid  4654  ordtri2or2exmid  4698  ontri2orexmidim  4699  iotaexab  5336  fununi  5429  funcnvuni  5430  feq3  5498  ssimaexg  5744  nnawordex  6775  ereq1  6787  xpider  6853  domeng  7002  ssfiexmid  7144  ssfiexmidt  7146  fisseneq  7208  sbthlemi4  7243  sbthlemi5  7244  nninfninc  7427  acfun  7527  onntri45  7564  ccfunen  7594  fprodssdc  12301  lspf  14663  lspval  14664  basis2  15039  eltg2  15044  clsval  15102  ntrcls0  15122  isnei  15135  neiint  15136  neipsm  15145  opnneissb  15146  opnssneib  15147  innei  15154  icnpimaex  15202  cnptoprest2  15231  neitx  15259  txcnp  15262  blssps  15418  blss  15419  metss  15485  metrest  15497  metcnp3  15502  upgredgpr  16270  wlkvtxiedg  16466  wlkvtxiedgg  16467  wlkres  16500  bdssexg  16800  bj-nntrans  16847  bj-omtrans  16852