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  6697  ereq1  6709  xpider  6775  domeng  6923  ssfiexmid  7063  ssfiexmidt  7065  fisseneq  7127  sbthlemi4  7159  sbthlemi5  7160  nninfninc  7322  acfun  7422  onntri45  7459  ccfunen  7483  fprodssdc  12169  lspf  14422  lspval  14423  basis2  14791  eltg2  14796  clsval  14854  ntrcls0  14874  isnei  14887  neiint  14888  neipsm  14897  opnneissb  14898  opnssneib  14899  innei  14906  icnpimaex  14954  cnptoprest2  14983  neitx  15011  txcnp  15014  blssps  15170  blss  15171  metss  15237  metrest  15249  metcnp3  15254  upgredgpr  16019  wlkvtxiedg  16215  wlkvtxiedgg  16216  wlkres  16249  bdssexg  16550  bj-nntrans  16597  bj-omtrans  16602