Theorem sseq1 3248

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 3240	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3232	. . . 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 3232	. . . 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 3198

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 3204  df-ss 3211

This theorem is referenced by:  sseq12  3250  sseq1i  3251  sseq1d  3254  nssne2  3284  sbss  3600  pwjust  3651  elpw  3656  elpwg  3658  sssnr  3834  ssprr  3837  sstpr  3838  unimax  3925  trss  4194  elssabg  4236  bnd2  4261  exmidexmid  4284  exmidsssn  4290  exmidsssnc  4291  exmid1stab  4296  mss  4316  exss  4317  frforeq2  4440  ordtri2orexmid  4619  ontr2exmid  4621  onsucsssucexmid  4623  reg2exmidlema  4630  sucprcreg  4645  ordtri2or2exmid  4667  ontri2orexmidim  4668  onintexmid  4669  tfis  4679  tfisi  4683  elomssom  4701  nnregexmid  4717  releq  4806  xpsspw  4836  iss  5057  relcnvtr  5254  iotass  5302  fununi  5395  funcnvuni  5396  funimaexglem  5410  ffoss  5612  ssimaex  5703  tfrlem1  6469  el2oss1o  6606  nnsucsssuc  6655  qsss  6758  phpm  7047  ssfiexmid  7058  findcard2d  7073  findcard2sd  7074  diffifi  7076  isinfinf  7079  fiintim  7116  fisseneq  7119  fidcenumlemrk  7144  fidcenumlemr  7145  sbthlem2  7148  isbth  7157  ctssdclemr  7302  onntri45  7449  tapeq1  7461  elinp  7684  sup3exmid  9127  zfz1isolem1  11094  zfz1iso  11095  fimaxre2  11778  sumeq1  11906  fsum2d  11986  fsumabs  12016  fsumiun  12028  prodeq1f  12103  fprod2d  12174  exmidunben  13037  ctiunct  13051  ssomct  13056  restsspw  13322  lspval  14394  uniopn  14715  fiinopn  14718  fiinbas  14763  baspartn  14764  eltg2  14767  eltg3  14771  topbas  14781  clsval  14825  neival  14857  neiint  14859  neipsm  14868  opnneissb  14869  opnssneib  14870  innei  14877  restbasg  14882  cnpdis  14956  txbas  14972  eltx  14973  neitx  14982  txlm  14993  blssexps  15143  blssex  15144  neibl  15205  metrest  15220  xmettx  15224  tgioo  15268  tgqioo  15269  limcimolemlt  15378  recnprss  15401  dvmptfsum  15439  lpvtx  15920  bj-om  16468  bj-2inf  16469  bj-nntrans  16482  bj-omtrans  16487  subctctexmid  16537  domomsubct  16538  pw1nct  16540