Theorem sseq1 3178

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 3170	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3162	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 277	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3162	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 276	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6	3, 5	impbid 129	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7	1, 6	sylbi 121	1 |- ( A = B -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1353   C_ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  sseq12  3180  sseq1i  3181  sseq1d  3184  nssne2  3214  sbss  3531  pwjust  3576  elpw  3581  elpwg  3583  sssnr  3753  ssprr  3756  sstpr  3757  unimax  3843  trss  4110  elssabg  4148  bnd2  4173  exmidexmid  4196  exmidsssn  4202  exmidsssnc  4203  exmid1stab  4208  mss  4226  exss  4227  frforeq2  4345  ordtri2orexmid  4522  ontr2exmid  4524  onsucsssucexmid  4526  reg2exmidlema  4533  sucprcreg  4548  ordtri2or2exmid  4570  ontri2orexmidim  4571  onintexmid  4572  tfis  4582  tfisi  4586  elomssom  4604  nnregexmid  4620  releq  4708  xpsspw  4738  iss  4953  relcnvtr  5148  iotass  5195  fununi  5284  funcnvuni  5285  funimaexglem  5299  ffoss  5493  ssimaex  5577  tfrlem1  6308  el2oss1o  6443  nnsucsssuc  6492  qsss  6593  phpm  6864  ssfiexmid  6875  findcard2d  6890  findcard2sd  6891  diffifi  6893  isinfinf  6896  fiintim  6927  fisseneq  6930  fidcenumlemrk  6952  fidcenumlemr  6953  sbthlem2  6956  isbth  6965  ctssdclemr  7110  onntri45  7239  tapeq1  7250  elinp  7472  sup3exmid  8913  zfz1isolem1  10819  zfz1iso  10820  fimaxre2  11234  sumeq1  11362  fsum2d  11442  fsumabs  11472  fsumiun  11484  prodeq1f  11559  fprod2d  11630  exmidunben  12426  ctiunct  12440  ssomct  12445  restsspw  12697  uniopn  13471  fiinopn  13474  fiinbas  13519  baspartn  13520  eltg2  13523  eltg3  13527  topbas  13537  clsval  13581  neival  13613  neiint  13615  neipsm  13624  opnneissb  13625  opnssneib  13626  innei  13633  restbasg  13638  cnpdis  13712  txbas  13728  eltx  13729  neitx  13738  txlm  13749  blssexps  13899  blssex  13900  neibl  13961  metrest  13976  xmettx  13980  tgioo  14016  tgqioo  14017  limcimolemlt  14103  recnprss  14126  bj-om  14659  bj-2inf  14660  bj-nntrans  14673  bj-omtrans  14678  subctctexmid  14720  pw1nct  14722