Theorem sseq1 3247

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 3239	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3231	. . . 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 3231	. . . 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 1395   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sseq12  3249  sseq1i  3250  sseq1d  3253  nssne2  3283  sbss  3599  pwjust  3650  elpw  3655  elpwg  3657  sssnr  3830  ssprr  3833  sstpr  3834  unimax  3921  trss  4190  elssabg  4231  bnd2  4256  exmidexmid  4279  exmidsssn  4285  exmidsssnc  4286  exmid1stab  4291  mss  4311  exss  4312  frforeq2  4435  ordtri2orexmid  4614  ontr2exmid  4616  onsucsssucexmid  4618  reg2exmidlema  4625  sucprcreg  4640  ordtri2or2exmid  4662  ontri2orexmidim  4663  onintexmid  4664  tfis  4674  tfisi  4678  elomssom  4696  nnregexmid  4712  releq  4800  xpsspw  4830  iss  5050  relcnvtr  5247  iotass  5295  fununi  5388  funcnvuni  5389  funimaexglem  5403  ffoss  5603  ssimaex  5694  tfrlem1  6452  el2oss1o  6587  nnsucsssuc  6636  qsss  6739  phpm  7023  ssfiexmid  7034  findcard2d  7049  findcard2sd  7050  diffifi  7052  isinfinf  7055  fiintim  7089  fisseneq  7092  fidcenumlemrk  7117  fidcenumlemr  7118  sbthlem2  7121  isbth  7130  ctssdclemr  7275  onntri45  7422  tapeq1  7434  elinp  7657  sup3exmid  9100  zfz1isolem1  11057  zfz1iso  11058  fimaxre2  11733  sumeq1  11861  fsum2d  11941  fsumabs  11971  fsumiun  11983  prodeq1f  12058  fprod2d  12129  exmidunben  12992  ctiunct  13006  ssomct  13011  restsspw  13277  lspval  14348  uniopn  14669  fiinopn  14672  fiinbas  14717  baspartn  14718  eltg2  14721  eltg3  14725  topbas  14735  clsval  14779  neival  14811  neiint  14813  neipsm  14822  opnneissb  14823  opnssneib  14824  innei  14831  restbasg  14836  cnpdis  14910  txbas  14926  eltx  14927  neitx  14936  txlm  14947  blssexps  15097  blssex  15098  neibl  15159  metrest  15174  xmettx  15178  tgioo  15222  tgqioo  15223  limcimolemlt  15332  recnprss  15355  dvmptfsum  15393  lpvtx  15873  bj-om  16258  bj-2inf  16259  bj-nntrans  16272  bj-omtrans  16277  subctctexmid  16325  domomsubct  16326  pw1nct  16328