Theorem sseq1 3251

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 3243	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3235	. . . 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 3235	. . . 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 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sseq12  3253  sseq1i  3254  sseq1d  3257  nssne2  3287  sbss  3604  pwjust  3657  elpw  3662  elpwg  3664  sssnr  3841  ssprr  3844  sstpr  3845  unimax  3932  trss  4201  elssabg  4243  bnd2  4269  exmidexmid  4292  exmidsssn  4298  exmidsssnc  4299  exmid1stab  4304  mss  4324  exss  4325  frforeq2  4448  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  reg2exmidlema  4638  sucprcreg  4653  ordtri2or2exmid  4675  ontri2orexmidim  4676  onintexmid  4677  tfis  4687  tfisi  4691  elomssom  4709  nnregexmid  4725  releq  4814  xpsspw  4844  iss  5065  relcnvtr  5263  iotass  5311  fununi  5405  funcnvuni  5406  funimaexglem  5420  ffoss  5625  ssimaex  5716  tfrlem1  6517  el2oss1o  6654  nnsucsssuc  6703  qsss  6806  phpm  7095  ssfiexmid  7106  ssfiexmidt  7108  findcard2d  7123  findcard2sd  7124  diffifi  7126  isinfinf  7129  fiintim  7166  fisseneq  7170  fidcenumlemrk  7196  fidcenumlemr  7197  sbthlem2  7200  isbth  7209  ctssdclemr  7354  onntri45  7502  tapeq1  7514  elinp  7737  sup3exmid  9179  zfz1isolem1  11150  zfz1iso  11151  fimaxre2  11850  sumeq1  11978  fsum2d  12059  fsumabs  12089  fsumiun  12101  prodeq1f  12176  fprod2d  12247  exmidunben  13110  ctiunct  13124  ssomct  13129  restsspw  13395  lspval  14469  uniopn  14795  fiinopn  14798  fiinbas  14843  baspartn  14844  eltg2  14847  eltg3  14851  topbas  14861  clsval  14905  neival  14937  neiint  14939  neipsm  14948  opnneissb  14949  opnssneib  14950  innei  14957  restbasg  14962  cnpdis  15036  txbas  15052  eltx  15053  neitx  15062  txlm  15073  blssexps  15223  blssex  15224  neibl  15285  metrest  15300  xmettx  15304  tgioo  15348  tgqioo  15349  limcimolemlt  15458  recnprss  15481  dvmptfsum  15519  lpvtx  16003  issubgr2  16182  subgrprop2  16184  egrsubgr  16187  0uhgrsubgr  16189  bj-om  16636  bj-2inf  16637  bj-nntrans  16650  bj-omtrans  16655  subctctexmid  16705  domomsubct  16706  pw1nct  16708