Theorem sseq1 3170

Description: Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

Ref	Expression
sseq1	|- ( A = B -> ( A C_ C <-> B C_ C ) )

Proof of Theorem sseq1

Step	Hyp	Ref	Expression
1		eqss 3162	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3154	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 275	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3154	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 274	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6	3, 5	impbid 128	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7	1, 6	sylbi 120	1 |- ( A = B -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1348   C_ wss 3121

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  sseq12  3172  sseq1i  3173  sseq1d  3176  nssne2  3206  sbss  3523  pwjust  3567  elpw  3572  elpwg  3574  sssnr  3740  ssprr  3743  sstpr  3744  unimax  3830  trss  4096  elssabg  4134  bnd2  4159  exmidexmid  4182  exmidsssn  4188  exmidsssnc  4189  mss  4211  exss  4212  frforeq2  4330  ordtri2orexmid  4507  ontr2exmid  4509  onsucsssucexmid  4511  reg2exmidlema  4518  sucprcreg  4533  ordtri2or2exmid  4555  ontri2orexmidim  4556  onintexmid  4557  tfis  4567  tfisi  4571  elomssom  4589  nnregexmid  4605  releq  4693  xpsspw  4723  iss  4937  relcnvtr  5130  iotass  5177  fununi  5266  funcnvuni  5267  funimaexglem  5281  ffoss  5474  ssimaex  5557  tfrlem1  6287  el2oss1o  6422  nnsucsssuc  6471  qsss  6572  phpm  6843  ssfiexmid  6854  findcard2d  6869  findcard2sd  6870  diffifi  6872  isinfinf  6875  fiintim  6906  fisseneq  6909  fidcenumlemrk  6931  fidcenumlemr  6932  sbthlem2  6935  isbth  6944  ctssdclemr  7089  onntri45  7218  elinp  7436  sup3exmid  8873  zfz1isolem1  10775  zfz1iso  10776  fimaxre2  11190  sumeq1  11318  fsum2d  11398  fsumabs  11428  fsumiun  11440  prodeq1f  11515  fprod2d  11586  exmidunben  12381  ctiunct  12395  ssomct  12400  restsspw  12589  uniopn  12793  fiinopn  12796  fiinbas  12841  baspartn  12842  eltg2  12847  eltg3  12851  topbas  12861  clsval  12905  neival  12937  neiint  12939  neipsm  12948  opnneissb  12949  opnssneib  12950  innei  12957  restbasg  12962  cnpdis  13036  txbas  13052  eltx  13053  neitx  13062  txlm  13073  blssexps  13223  blssex  13224  neibl  13285  metrest  13300  xmettx  13304  tgioo  13340  tgqioo  13341  limcimolemlt  13427  recnprss  13450  bj-om  13972  bj-2inf  13973  bj-nntrans  13986  bj-omtrans  13991  exmid1stab  14033  subctctexmid  14034  pw1nct  14036