Theorem sseq1 3202

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 3194	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3186	. . . 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 3186	. . . 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 3153

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 3159  df-ss 3166

This theorem is referenced by:  sseq12  3204  sseq1i  3205  sseq1d  3208  nssne2  3238  sbss  3554  pwjust  3602  elpw  3607  elpwg  3609  sssnr  3779  ssprr  3782  sstpr  3783  unimax  3869  trss  4136  elssabg  4177  bnd2  4202  exmidexmid  4225  exmidsssn  4231  exmidsssnc  4232  exmid1stab  4237  mss  4255  exss  4256  frforeq2  4376  ordtri2orexmid  4555  ontr2exmid  4557  onsucsssucexmid  4559  reg2exmidlema  4566  sucprcreg  4581  ordtri2or2exmid  4603  ontri2orexmidim  4604  onintexmid  4605  tfis  4615  tfisi  4619  elomssom  4637  nnregexmid  4653  releq  4741  xpsspw  4771  iss  4988  relcnvtr  5185  iotass  5232  fununi  5322  funcnvuni  5323  funimaexglem  5337  ffoss  5532  ssimaex  5618  tfrlem1  6361  el2oss1o  6496  nnsucsssuc  6545  qsss  6648  phpm  6921  ssfiexmid  6932  findcard2d  6947  findcard2sd  6948  diffifi  6950  isinfinf  6953  fiintim  6985  fisseneq  6988  fidcenumlemrk  7013  fidcenumlemr  7014  sbthlem2  7017  isbth  7026  ctssdclemr  7171  onntri45  7301  tapeq1  7312  elinp  7534  sup3exmid  8976  zfz1isolem1  10911  zfz1iso  10912  fimaxre2  11370  sumeq1  11498  fsum2d  11578  fsumabs  11608  fsumiun  11620  prodeq1f  11695  fprod2d  11766  exmidunben  12583  ctiunct  12597  ssomct  12602  restsspw  12860  lspval  13886  uniopn  14169  fiinopn  14172  fiinbas  14217  baspartn  14218  eltg2  14221  eltg3  14225  topbas  14235  clsval  14279  neival  14311  neiint  14313  neipsm  14322  opnneissb  14323  opnssneib  14324  innei  14331  restbasg  14336  cnpdis  14410  txbas  14426  eltx  14427  neitx  14436  txlm  14447  blssexps  14597  blssex  14598  neibl  14659  metrest  14674  xmettx  14678  tgioo  14714  tgqioo  14715  limcimolemlt  14818  recnprss  14841  bj-om  15429  bj-2inf  15430  bj-nntrans  15443  bj-omtrans  15448  subctctexmid  15491  pw1nct  15493