Theorem sseq1 3203

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 3195	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3187	. . . 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 3187	. . . 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 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  sseq12  3205  sseq1i  3206  sseq1d  3209  nssne2  3239  sbss  3555  pwjust  3603  elpw  3608  elpwg  3610  sssnr  3780  ssprr  3783  sstpr  3784  unimax  3870  trss  4137  elssabg  4178  bnd2  4203  exmidexmid  4226  exmidsssn  4232  exmidsssnc  4233  exmid1stab  4238  mss  4256  exss  4257  frforeq2  4377  ordtri2orexmid  4556  ontr2exmid  4558  onsucsssucexmid  4560  reg2exmidlema  4567  sucprcreg  4582  ordtri2or2exmid  4604  ontri2orexmidim  4605  onintexmid  4606  tfis  4616  tfisi  4620  elomssom  4638  nnregexmid  4654  releq  4742  xpsspw  4772  iss  4989  relcnvtr  5186  iotass  5233  fununi  5323  funcnvuni  5324  funimaexglem  5338  ffoss  5533  ssimaex  5619  tfrlem1  6363  el2oss1o  6498  nnsucsssuc  6547  qsss  6650  phpm  6923  ssfiexmid  6934  findcard2d  6949  findcard2sd  6950  diffifi  6952  isinfinf  6955  fiintim  6987  fisseneq  6990  fidcenumlemrk  7015  fidcenumlemr  7016  sbthlem2  7019  isbth  7028  ctssdclemr  7173  onntri45  7303  tapeq1  7314  elinp  7536  sup3exmid  8978  zfz1isolem1  10914  zfz1iso  10915  fimaxre2  11373  sumeq1  11501  fsum2d  11581  fsumabs  11611  fsumiun  11623  prodeq1f  11698  fprod2d  11769  exmidunben  12586  ctiunct  12600  ssomct  12605  restsspw  12863  lspval  13889  uniopn  14180  fiinopn  14183  fiinbas  14228  baspartn  14229  eltg2  14232  eltg3  14236  topbas  14246  clsval  14290  neival  14322  neiint  14324  neipsm  14333  opnneissb  14334  opnssneib  14335  innei  14342  restbasg  14347  cnpdis  14421  txbas  14437  eltx  14438  neitx  14447  txlm  14458  blssexps  14608  blssex  14609  neibl  14670  metrest  14685  xmettx  14689  tgioo  14733  tgqioo  14734  limcimolemlt  14843  recnprss  14866  dvmptfsum  14904  bj-om  15499  bj-2inf  15500  bj-nntrans  15513  bj-omtrans  15518  subctctexmid  15561  pw1nct  15563