Theorem sseq1 3215

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 3207	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3199	. . . 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 3199	. . . 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 1372   C_ wss 3165

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-11 1528  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-in 3171  df-ss 3178

This theorem is referenced by:  sseq12  3217  sseq1i  3218  sseq1d  3221  nssne2  3251  sbss  3567  pwjust  3616  elpw  3621  elpwg  3623  sssnr  3793  ssprr  3796  sstpr  3797  unimax  3883  trss  4150  elssabg  4191  bnd2  4216  exmidexmid  4239  exmidsssn  4245  exmidsssnc  4246  exmid1stab  4251  mss  4269  exss  4270  frforeq2  4391  ordtri2orexmid  4570  ontr2exmid  4572  onsucsssucexmid  4574  reg2exmidlema  4581  sucprcreg  4596  ordtri2or2exmid  4618  ontri2orexmidim  4619  onintexmid  4620  tfis  4630  tfisi  4634  elomssom  4652  nnregexmid  4668  releq  4756  xpsspw  4786  iss  5004  relcnvtr  5201  iotass  5248  fununi  5341  funcnvuni  5342  funimaexglem  5356  ffoss  5553  ssimaex  5639  tfrlem1  6393  el2oss1o  6528  nnsucsssuc  6577  qsss  6680  phpm  6961  ssfiexmid  6972  findcard2d  6987  findcard2sd  6988  diffifi  6990  isinfinf  6993  fiintim  7027  fisseneq  7030  fidcenumlemrk  7055  fidcenumlemr  7056  sbthlem2  7059  isbth  7068  ctssdclemr  7213  onntri45  7352  tapeq1  7363  elinp  7586  sup3exmid  9029  zfz1isolem1  10983  zfz1iso  10984  fimaxre2  11509  sumeq1  11637  fsum2d  11717  fsumabs  11747  fsumiun  11759  prodeq1f  11834  fprod2d  11905  exmidunben  12768  ctiunct  12782  ssomct  12787  restsspw  13052  lspval  14123  uniopn  14444  fiinopn  14447  fiinbas  14492  baspartn  14493  eltg2  14496  eltg3  14500  topbas  14510  clsval  14554  neival  14586  neiint  14588  neipsm  14597  opnneissb  14598  opnssneib  14599  innei  14606  restbasg  14611  cnpdis  14685  txbas  14701  eltx  14702  neitx  14711  txlm  14722  blssexps  14872  blssex  14873  neibl  14934  metrest  14949  xmettx  14953  tgioo  14997  tgqioo  14998  limcimolemlt  15107  recnprss  15130  dvmptfsum  15168  bj-om  15835  bj-2inf  15836  bj-nntrans  15849  bj-omtrans  15854  subctctexmid  15899  domomsubct  15900  pw1nct  15902