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  12153  lspf  14406  lspval  14407  basis2  14775  eltg2  14780  clsval  14838  ntrcls0  14858  isnei  14871  neiint  14872  neipsm  14881  opnneissb  14882  opnssneib  14883  innei  14890  icnpimaex  14938  cnptoprest2  14967  neitx  14995  txcnp  14998  blssps  15154  blss  15155  metss  15221  metrest  15233  metcnp3  15238  upgredgpr  16003  wlkvtxiedg  16199  wlkvtxiedgg  16200  wlkres  16233  bdssexg  16516  bj-nntrans  16563  bj-omtrans  16568