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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   C_ wss 3220

This proof depends on 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 proof 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 used by:  sseq12  3273  sseq1i  3274  sseq1d  3277  nssne2  3307  vvin  3569  sbss  3635  pwjust  3689  elpw  3694  elpwg  3696  sssnr  3878  ssprr  3881  sstpr  3882  unimax  3969  trss  4238  elssabg  4284  bnd2  4310  exmidexmid  4333  exmidsssn  4339  exmidsssnc  4340  exmid1stab  4345  mss  4366  exss  4367  frforeq2  4490  ordtri2orexmid  4670  ontr2exmid  4672  onsucsssucexmid  4674  reg2exmidlema  4681  sucprcreg  4696  ordtri2or2exmid  4718  ontri2orexmidim  4719  onintexmid  4720  tfis  4730  tfisi  4734  elomssom  4752  nnregexmid  4768  releq  4857  xpsspw  4887  iss  5109  relcnvtr  5307  iotass  5355  fununi  5449  funcnvuni  5450  funimaexglem  5464  ffoss  5672  ssimaex  5764  tfrlem1  6579  el2oss1o  6716  nnsucsssuc  6765  qsss  6868  phpm  7167  ssfiexmid  7178  ssfiexmidt  7180  findcard2d  7195  findcard2sd  7196  diffifi  7198  isinfinf  7201  fiintim  7238  fisseneq  7242  fidcenumlemrk  7271  fidcenumlemr  7272  sbthlem2  7275  isbth  7284  ctssdclemr  7452  onntri45  7600  papeq1  7609  tapeq1  7618  elinp  7841  sup3exmid  9287  zfz1isolem1  11292  zfz1iso  11293  fimaxre2  11993  sumeq1  12121  fsum2d  12202  fsumabs  12232  fsumiun  12244  prodeq1f  12319  fprod2d  12390  exmidunben  13317  ctiunct  13331  ssomct  13336  restsspw  13603  lspval  14727  aspval  15015  uniopn  15102  fiinopn  15105  fiinbas  15150  baspartn  15151  eltg2  15154  eltg3  15158  topbas  15168  clsval  15212  neival  15244  neiint  15246  neipsm  15255  opnneissb  15256  opnssneib  15257  innei  15264  restbasg  15269  cnpdis  15343  txbas  15359  eltx  15360  neitx  15369  txlm  15380  blssexps  15530  blssex  15531  neibl  15592  metrest  15607  xmettx  15611  tgioo  15655  tgqioo  15656  limcimolemlt  15765  recnprss  15788  dvmptfsum  15826  lpvtx  16320  issubgr2  16499  subgrprop2  16501  egrsubgr  16504  0uhgrsubgr  16506  bj-om  16963  bj-2inf  16964  bj-nntrans  16977  bj-omtrans  16982  subctctexmid  17030  domomsubct  17031  pw1nct  17033