Theorem sseq1 3250

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 3242	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3234	. . . 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 3234	. . . 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 1397   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  sseq12  3252  sseq1i  3253  sseq1d  3256  nssne2  3286  sbss  3602  pwjust  3653  elpw  3658  elpwg  3660  sssnr  3836  ssprr  3839  sstpr  3840  unimax  3927  trss  4196  elssabg  4238  bnd2  4263  exmidexmid  4286  exmidsssn  4292  exmidsssnc  4293  exmid1stab  4298  mss  4318  exss  4319  frforeq2  4442  ordtri2orexmid  4621  ontr2exmid  4623  onsucsssucexmid  4625  reg2exmidlema  4632  sucprcreg  4647  ordtri2or2exmid  4669  ontri2orexmidim  4670  onintexmid  4671  tfis  4681  tfisi  4685  elomssom  4703  nnregexmid  4719  releq  4808  xpsspw  4838  iss  5059  relcnvtr  5256  iotass  5304  fununi  5398  funcnvuni  5399  funimaexglem  5413  ffoss  5616  ssimaex  5707  tfrlem1  6473  el2oss1o  6610  nnsucsssuc  6659  qsss  6762  phpm  7051  ssfiexmid  7062  ssfiexmidt  7064  findcard2d  7079  findcard2sd  7080  diffifi  7082  isinfinf  7085  fiintim  7122  fisseneq  7126  fidcenumlemrk  7152  fidcenumlemr  7153  sbthlem2  7156  isbth  7165  ctssdclemr  7310  onntri45  7458  tapeq1  7470  elinp  7693  sup3exmid  9136  zfz1isolem1  11103  zfz1iso  11104  fimaxre2  11787  sumeq1  11915  fsum2d  11995  fsumabs  12025  fsumiun  12037  prodeq1f  12112  fprod2d  12183  exmidunben  13046  ctiunct  13060  ssomct  13065  restsspw  13331  lspval  14403  uniopn  14724  fiinopn  14727  fiinbas  14772  baspartn  14773  eltg2  14776  eltg3  14780  topbas  14790  clsval  14834  neival  14866  neiint  14868  neipsm  14877  opnneissb  14878  opnssneib  14879  innei  14886  restbasg  14891  cnpdis  14965  txbas  14981  eltx  14982  neitx  14991  txlm  15002  blssexps  15152  blssex  15153  neibl  15214  metrest  15229  xmettx  15233  tgioo  15277  tgqioo  15278  limcimolemlt  15387  recnprss  15410  dvmptfsum  15448  lpvtx  15929  issubgr2  16108  subgrprop2  16110  egrsubgr  16113  0uhgrsubgr  16115  bj-om  16532  bj-2inf  16533  bj-nntrans  16546  bj-omtrans  16551  subctctexmid  16601  domomsubct  16602  pw1nct  16604