Theorem sseq1 3207

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 3199	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3191	. . . 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 3191	. . . 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 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sseq12  3209  sseq1i  3210  sseq1d  3213  nssne2  3243  sbss  3559  pwjust  3607  elpw  3612  elpwg  3614  sssnr  3784  ssprr  3787  sstpr  3788  unimax  3874  trss  4141  elssabg  4182  bnd2  4207  exmidexmid  4230  exmidsssn  4236  exmidsssnc  4237  exmid1stab  4242  mss  4260  exss  4261  frforeq2  4381  ordtri2orexmid  4560  ontr2exmid  4562  onsucsssucexmid  4564  reg2exmidlema  4571  sucprcreg  4586  ordtri2or2exmid  4608  ontri2orexmidim  4609  onintexmid  4610  tfis  4620  tfisi  4624  elomssom  4642  nnregexmid  4658  releq  4746  xpsspw  4776  iss  4993  relcnvtr  5190  iotass  5237  fununi  5327  funcnvuni  5328  funimaexglem  5342  ffoss  5539  ssimaex  5625  tfrlem1  6375  el2oss1o  6510  nnsucsssuc  6559  qsss  6662  phpm  6935  ssfiexmid  6946  findcard2d  6961  findcard2sd  6962  diffifi  6964  isinfinf  6967  fiintim  7001  fisseneq  7004  fidcenumlemrk  7029  fidcenumlemr  7030  sbthlem2  7033  isbth  7042  ctssdclemr  7187  onntri45  7324  tapeq1  7335  elinp  7558  sup3exmid  9001  zfz1isolem1  10949  zfz1iso  10950  fimaxre2  11409  sumeq1  11537  fsum2d  11617  fsumabs  11647  fsumiun  11659  prodeq1f  11734  fprod2d  11805  exmidunben  12668  ctiunct  12682  ssomct  12687  restsspw  12951  lspval  14022  uniopn  14321  fiinopn  14324  fiinbas  14369  baspartn  14370  eltg2  14373  eltg3  14377  topbas  14387  clsval  14431  neival  14463  neiint  14465  neipsm  14474  opnneissb  14475  opnssneib  14476  innei  14483  restbasg  14488  cnpdis  14562  txbas  14578  eltx  14579  neitx  14588  txlm  14599  blssexps  14749  blssex  14750  neibl  14811  metrest  14826  xmettx  14830  tgioo  14874  tgqioo  14875  limcimolemlt  14984  recnprss  15007  dvmptfsum  15045  bj-om  15667  bj-2inf  15668  bj-nntrans  15681  bj-omtrans  15686  subctctexmid  15731  domomsubct  15732  pw1nct  15734