Theorem sseq1 3261

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 3253	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3245	. . . 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 3245	. . . 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 1398   C_ wss 3211

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  sseq12  3263  sseq1i  3264  sseq1d  3267  nssne2  3297  sbss  3617  pwjust  3670  elpw  3675  elpwg  3677  sssnr  3857  ssprr  3860  sstpr  3861  unimax  3948  trss  4217  elssabg  4260  bnd2  4286  exmidexmid  4309  exmidsssn  4315  exmidsssnc  4316  exmid1stab  4321  mss  4342  exss  4343  frforeq2  4466  ordtri2orexmid  4645  ontr2exmid  4647  onsucsssucexmid  4649  reg2exmidlema  4656  sucprcreg  4671  ordtri2or2exmid  4693  ontri2orexmidim  4694  onintexmid  4695  tfis  4705  tfisi  4709  elomssom  4727  nnregexmid  4743  releq  4832  xpsspw  4862  iss  5084  relcnvtr  5282  iotass  5330  fununi  5424  funcnvuni  5425  funimaexglem  5439  ffoss  5647  ssimaex  5738  tfrlem1  6539  el2oss1o  6676  nnsucsssuc  6725  qsss  6828  phpm  7120  ssfiexmid  7131  ssfiexmidt  7133  findcard2d  7148  findcard2sd  7149  diffifi  7151  isinfinf  7154  fiintim  7191  fisseneq  7195  fidcenumlemrk  7224  fidcenumlemr  7225  sbthlem2  7228  isbth  7237  ctssdclemr  7403  onntri45  7551  tapeq1  7566  elinp  7789  sup3exmid  9231  zfz1isolem1  11212  zfz1iso  11213  fimaxre2  11912  sumeq1  12040  fsum2d  12121  fsumabs  12151  fsumiun  12163  prodeq1f  12238  fprod2d  12309  exmidunben  13177  ctiunct  13191  ssomct  13196  restsspw  13462  lspval  14538  uniopn  14866  fiinopn  14869  fiinbas  14914  baspartn  14915  eltg2  14918  eltg3  14922  topbas  14932  clsval  14976  neival  15008  neiint  15010  neipsm  15019  opnneissb  15020  opnssneib  15021  innei  15028  restbasg  15033  cnpdis  15107  txbas  15123  eltx  15124  neitx  15133  txlm  15144  blssexps  15294  blssex  15295  neibl  15356  metrest  15371  xmettx  15375  tgioo  15419  tgqioo  15420  limcimolemlt  15529  recnprss  15552  dvmptfsum  15590  lpvtx  16074  issubgr2  16253  subgrprop2  16255  egrsubgr  16258  0uhgrsubgr  16260  bj-om  16707  bj-2inf  16708  bj-nntrans  16721  bj-omtrans  16726  subctctexmid  16774  domomsubct  16775  pw1nct  16777