Theorem sseq1 3193

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 3185	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3177	. . . 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 3177	. . . 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 1364   C_ wss 3144

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-in 3150  df-ss 3157

This theorem is referenced by:  sseq12  3195  sseq1i  3196  sseq1d  3199  nssne2  3229  sbss  3546  pwjust  3591  elpw  3596  elpwg  3598  sssnr  3768  ssprr  3771  sstpr  3772  unimax  3858  trss  4125  elssabg  4166  bnd2  4191  exmidexmid  4214  exmidsssn  4220  exmidsssnc  4221  exmid1stab  4226  mss  4244  exss  4245  frforeq2  4363  ordtri2orexmid  4540  ontr2exmid  4542  onsucsssucexmid  4544  reg2exmidlema  4551  sucprcreg  4566  ordtri2or2exmid  4588  ontri2orexmidim  4589  onintexmid  4590  tfis  4600  tfisi  4604  elomssom  4622  nnregexmid  4638  releq  4726  xpsspw  4756  iss  4971  relcnvtr  5166  iotass  5213  fununi  5303  funcnvuni  5304  funimaexglem  5318  ffoss  5512  ssimaex  5598  tfrlem1  6334  el2oss1o  6469  nnsucsssuc  6518  qsss  6621  phpm  6894  ssfiexmid  6905  findcard2d  6920  findcard2sd  6921  diffifi  6923  isinfinf  6926  fiintim  6958  fisseneq  6961  fidcenumlemrk  6984  fidcenumlemr  6985  sbthlem2  6988  isbth  6997  ctssdclemr  7142  onntri45  7271  tapeq1  7282  elinp  7504  sup3exmid  8945  zfz1isolem1  10855  zfz1iso  10856  fimaxre2  11270  sumeq1  11398  fsum2d  11478  fsumabs  11508  fsumiun  11520  prodeq1f  11595  fprod2d  11666  exmidunben  12480  ctiunct  12494  ssomct  12499  restsspw  12757  lspval  13723  uniopn  13978  fiinopn  13981  fiinbas  14026  baspartn  14027  eltg2  14030  eltg3  14034  topbas  14044  clsval  14088  neival  14120  neiint  14122  neipsm  14131  opnneissb  14132  opnssneib  14133  innei  14140  restbasg  14145  cnpdis  14219  txbas  14235  eltx  14236  neitx  14245  txlm  14256  blssexps  14406  blssex  14407  neibl  14468  metrest  14483  xmettx  14487  tgioo  14523  tgqioo  14524  limcimolemlt  14610  recnprss  14633  bj-om  15167  bj-2inf  15168  bj-nntrans  15181  bj-omtrans  15186  subctctexmid  15229  pw1nct  15231