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  7453  onntri45  7601  papeq1  7610  tapeq1  7619  elinp  7842  sup3exmid  9290  zfz1isolem1  11308  zfz1iso  11309  fimaxre2  12010  sumeq1  12140  fsum2d  12221  fsumabs  12251  fsumiun  12263  prodeq1f  12338  fprod2d  12409  exmidunben  13369  ctiunct  13383  ssomct  13388  restsspw  13656  lspval  14811  aspval  15099  uniopn  15193  fiinopn  15196  fiinbas  15241  baspartn  15242  eltg2  15245  eltg3  15249  topbas  15259  clsval  15303  neival  15335  neiint  15337  neipsm  15346  opnneissb  15347  opnssneib  15348  innei  15355  restbasg  15360  cnpdis  15434  txbas  15450  eltx  15451  neitx  15460  txlm  15471  blssexps  15621  blssex  15622  neibl  15683  metrest  15698  xmettx  15702  tgioo  15746  tgqioo  15747  limcimolemlt  15856  recnprss  15879  dvmptfsum  15917  lpvtx  16486  issubgr2  16665  subgrprop2  16667  egrsubgr  16670  0uhgrsubgr  16672  bj-om  17129  bj-2inf  17130  bj-nntrans  17143  bj-omtrans  17148  subctctexmid  17196  domomsubct  17197  pw1nct  17199