Theorem sseq2 3251

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 3234	. . . 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 3234	. . . 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 3242	. 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 1397   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sseq12  3252  sseq2i  3254  sseq2d  3257  sseqtrid  3277  nssne1  3285  sseq0  3536  un00  3541  pweq  3655  ssintab  3945  ssintub  3946  intmin  3948  treq  4193  ssexg  4228  exmidundif  4296  frforeq3  4444  frirrg  4447  iunpw  4577  ordtri2orexmid  4621  ontr2exmid  4623  onsucsssucexmid  4625  ordtri2or2exmid  4669  ontri2orexmidim  4670  iotaexab  5305  fununi  5398  funcnvuni  5399  feq3  5467  ssimaexg  5708  nnawordex  6696  ereq1  6708  xpider  6774  domeng  6922  ssfiexmid  7062  ssfiexmidt  7064  fisseneq  7126  sbthlemi4  7158  sbthlemi5  7159  nninfninc  7321  acfun  7421  onntri45  7458  ccfunen  7482  fprodssdc  12150  lspf  14402  lspval  14403  basis2  14771  eltg2  14776  clsval  14834  ntrcls0  14854  isnei  14867  neiint  14868  neipsm  14877  opnneissb  14878  opnssneib  14879  innei  14886  icnpimaex  14934  cnptoprest2  14963  neitx  14991  txcnp  14994  blssps  15150  blss  15151  metss  15217  metrest  15229  metcnp3  15234  upgredgpr  15999  wlkvtxiedg  16195  wlkvtxiedgg  16196  wlkres  16229  bdssexg  16499  bj-nntrans  16546  bj-omtrans  16551