Theorem sseq1 3224

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 3216	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3208	. . . 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 3208	. . . 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 1373   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  sseq12  3226  sseq1i  3227  sseq1d  3230  nssne2  3260  sbss  3576  pwjust  3627  elpw  3632  elpwg  3634  sssnr  3807  ssprr  3810  sstpr  3811  unimax  3898  trss  4167  elssabg  4208  bnd2  4233  exmidexmid  4256  exmidsssn  4262  exmidsssnc  4263  exmid1stab  4268  mss  4288  exss  4289  frforeq2  4410  ordtri2orexmid  4589  ontr2exmid  4591  onsucsssucexmid  4593  reg2exmidlema  4600  sucprcreg  4615  ordtri2or2exmid  4637  ontri2orexmidim  4638  onintexmid  4639  tfis  4649  tfisi  4653  elomssom  4671  nnregexmid  4687  releq  4775  xpsspw  4805  iss  5024  relcnvtr  5221  iotass  5268  fununi  5361  funcnvuni  5362  funimaexglem  5376  ffoss  5576  ssimaex  5663  tfrlem1  6417  el2oss1o  6552  nnsucsssuc  6601  qsss  6704  phpm  6988  ssfiexmid  6999  findcard2d  7014  findcard2sd  7015  diffifi  7017  isinfinf  7020  fiintim  7054  fisseneq  7057  fidcenumlemrk  7082  fidcenumlemr  7083  sbthlem2  7086  isbth  7095  ctssdclemr  7240  onntri45  7387  tapeq1  7399  elinp  7622  sup3exmid  9065  zfz1isolem1  11022  zfz1iso  11023  fimaxre2  11653  sumeq1  11781  fsum2d  11861  fsumabs  11891  fsumiun  11903  prodeq1f  11978  fprod2d  12049  exmidunben  12912  ctiunct  12926  ssomct  12931  restsspw  13196  lspval  14267  uniopn  14588  fiinopn  14591  fiinbas  14636  baspartn  14637  eltg2  14640  eltg3  14644  topbas  14654  clsval  14698  neival  14730  neiint  14732  neipsm  14741  opnneissb  14742  opnssneib  14743  innei  14750  restbasg  14755  cnpdis  14829  txbas  14845  eltx  14846  neitx  14855  txlm  14866  blssexps  15016  blssex  15017  neibl  15078  metrest  15093  xmettx  15097  tgioo  15141  tgqioo  15142  limcimolemlt  15251  recnprss  15274  dvmptfsum  15312  lpvtx  15790  bj-om  16072  bj-2inf  16073  bj-nntrans  16086  bj-omtrans  16091  subctctexmid  16139  domomsubct  16140  pw1nct  16142