Theorem sseq1 3271

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 3263	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3255	. . . 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 3255	. . . 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 1402   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  sseq12  3273  sseq1i  3274  sseq1d  3277  nssne2  3307  vvin  3568  sbss  3632  pwjust  3686  elpw  3691  elpwg  3693  sssnr  3873  ssprr  3876  sstpr  3877  unimax  3964  trss  4233  elssabg  4279  bnd2  4305  exmidexmid  4328  exmidsssn  4334  exmidsssnc  4335  exmid1stab  4340  mss  4361  exss  4362  frforeq2  4485  ordtri2orexmid  4665  ontr2exmid  4667  onsucsssucexmid  4669  reg2exmidlema  4676  sucprcreg  4691  ordtri2or2exmid  4713  ontri2orexmidim  4714  onintexmid  4715  tfis  4725  tfisi  4729  elomssom  4747  nnregexmid  4763  releq  4852  xpsspw  4882  iss  5104  relcnvtr  5302  iotass  5350  fununi  5444  funcnvuni  5445  funimaexglem  5459  ffoss  5667  ssimaex  5758  tfrlem1  6569  el2oss1o  6706  nnsucsssuc  6755  qsss  6858  phpm  7157  ssfiexmid  7168  ssfiexmidt  7170  findcard2d  7185  findcard2sd  7186  diffifi  7188  isinfinf  7191  fiintim  7228  fisseneq  7232  fidcenumlemrk  7261  fidcenumlemr  7262  sbthlem2  7265  isbth  7274  ctssdclemr  7442  onntri45  7590  papeq1  7599  tapeq1  7608  elinp  7831  sup3exmid  9277  zfz1isolem1  11270  zfz1iso  11271  fimaxre2  11971  sumeq1  12099  fsum2d  12180  fsumabs  12210  fsumiun  12222  prodeq1f  12297  fprod2d  12368  exmidunben  13295  ctiunct  13309  ssomct  13314  restsspw  13580  lspval  14699  uniopn  15025  fiinopn  15028  fiinbas  15073  baspartn  15074  eltg2  15077  eltg3  15081  topbas  15091  clsval  15135  neival  15167  neiint  15169  neipsm  15178  opnneissb  15179  opnssneib  15180  innei  15187  restbasg  15192  cnpdis  15266  txbas  15282  eltx  15283  neitx  15292  txlm  15303  blssexps  15453  blssex  15454  neibl  15515  metrest  15530  xmettx  15534  tgioo  15578  tgqioo  15579  limcimolemlt  15688  recnprss  15711  dvmptfsum  15749  lpvtx  16234  issubgr2  16413  subgrprop2  16415  egrsubgr  16418  0uhgrsubgr  16420  bj-om  16877  bj-2inf  16878  bj-nntrans  16891  bj-omtrans  16896  subctctexmid  16944  domomsubct  16945  pw1nct  16947