Theorem sseq1 3151

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 3143	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3135	. . . 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 3135	. . . 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 1335   C_ wss 3102

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  sseq12  3153  sseq1i  3154  sseq1d  3157  nssne2  3187  sbss  3502  pwjust  3544  elpw  3549  elpwg  3551  sssnr  3716  ssprr  3719  sstpr  3720  unimax  3806  trss  4071  elssabg  4109  bnd2  4134  exmidexmid  4157  exmidsssn  4163  exmidsssnc  4164  mss  4186  exss  4187  frforeq2  4305  ordtri2orexmid  4482  ontr2exmid  4484  onsucsssucexmid  4486  reg2exmidlema  4493  sucprcreg  4508  ordtri2or2exmid  4530  ontri2orexmidim  4531  onintexmid  4532  tfis  4542  tfisi  4546  elomssom  4564  nnregexmid  4580  releq  4668  xpsspw  4698  iss  4912  relcnvtr  5105  iotass  5152  fununi  5238  funcnvuni  5239  funimaexglem  5253  ffoss  5446  ssimaex  5529  tfrlem1  6255  el2oss1o  6390  nnsucsssuc  6439  qsss  6539  phpm  6810  ssfiexmid  6821  findcard2d  6836  findcard2sd  6837  diffifi  6839  isinfinf  6842  fiintim  6873  fisseneq  6876  fidcenumlemrk  6898  fidcenumlemr  6899  sbthlem2  6902  isbth  6911  ctssdclemr  7056  onntri45  7176  elinp  7394  sup3exmid  8828  zfz1isolem1  10711  zfz1iso  10712  fimaxre2  11126  sumeq1  11252  fsum2d  11332  fsumabs  11362  fsumiun  11374  prodeq1f  11449  fprod2d  11520  exmidunben  12166  ctiunct  12180  ssomct  12185  restsspw  12372  uniopn  12410  fiinopn  12413  fiinbas  12458  baspartn  12459  eltg2  12464  eltg3  12468  topbas  12478  clsval  12522  neival  12554  neiint  12556  neipsm  12565  opnneissb  12566  opnssneib  12567  innei  12574  restbasg  12579  cnpdis  12653  txbas  12669  eltx  12670  neitx  12679  txlm  12690  blssexps  12840  blssex  12841  neibl  12902  metrest  12917  xmettx  12921  tgioo  12957  tgqioo  12958  limcimolemlt  13044  recnprss  13067  bj-om  13523  bj-2inf  13524  bj-nntrans  13537  bj-omtrans  13542  exmid1stab  13583  subctctexmid  13584  pw1nct  13586