Theorem sseq1 3125

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 3117	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3109	. . . 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 3109	. . . 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 1332   C_ wss 3076

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  sseq12  3127  sseq1i  3128  sseq1d  3131  nssne2  3161  sbss  3476  pwjust  3516  elpw  3521  elpwg  3523  sssnr  3688  ssprr  3691  sstpr  3692  unimax  3778  trss  4043  elssabg  4081  bnd2  4105  exmidexmid  4128  exmidsssn  4133  exmidsssnc  4134  mss  4156  exss  4157  frforeq2  4275  ordtri2orexmid  4446  ontr2exmid  4448  onsucsssucexmid  4450  reg2exmidlema  4457  sucprcreg  4472  ordtri2or2exmid  4494  onintexmid  4495  tfis  4505  tfisi  4509  elnn  4527  nnregexmid  4542  releq  4629  xpsspw  4659  iss  4873  relcnvtr  5066  iotass  5113  fununi  5199  funcnvuni  5200  funimaexglem  5214  ffoss  5407  ssimaex  5490  tfrlem1  6213  nnsucsssuc  6396  qsss  6496  phpm  6767  ssfiexmid  6778  findcard2d  6793  findcard2sd  6794  diffifi  6796  isinfinf  6799  fiintim  6825  fisseneq  6828  fidcenumlemrk  6850  fidcenumlemr  6851  sbthlem2  6854  isbth  6863  ctssdclemr  7005  elinp  7306  sup3exmid  8739  zfz1isolem1  10615  zfz1iso  10616  fimaxre2  11030  sumeq1  11156  fsum2d  11236  fsumabs  11266  fsumiun  11278  prodeq1f  11353  exmidunben  11975  ctiunct  11989  restsspw  12169  uniopn  12207  fiinopn  12210  fiinbas  12255  baspartn  12256  eltg2  12261  eltg3  12265  topbas  12275  clsval  12319  neival  12351  neiint  12353  neipsm  12362  opnneissb  12363  opnssneib  12364  innei  12371  restbasg  12376  cnpdis  12450  txbas  12466  eltx  12467  neitx  12476  txlm  12487  blssexps  12637  blssex  12638  neibl  12699  metrest  12714  xmettx  12718  tgioo  12754  tgqioo  12755  limcimolemlt  12841  recnprss  12864  bj-om  13306  bj-2inf  13307  bj-nntrans  13320  bj-omtrans  13325  el2oss1o  13359  exmid1stab  13368  subctctexmid  13369  pw1nct  13371