Theorem sseq1 3216

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 3208	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3200	. . . 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 3200	. . . 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 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  sseq12  3218  sseq1i  3219  sseq1d  3222  nssne2  3252  sbss  3568  pwjust  3617  elpw  3622  elpwg  3624  sssnr  3794  ssprr  3797  sstpr  3798  unimax  3884  trss  4151  elssabg  4192  bnd2  4217  exmidexmid  4240  exmidsssn  4246  exmidsssnc  4247  exmid1stab  4252  mss  4270  exss  4271  frforeq2  4392  ordtri2orexmid  4571  ontr2exmid  4573  onsucsssucexmid  4575  reg2exmidlema  4582  sucprcreg  4597  ordtri2or2exmid  4619  ontri2orexmidim  4620  onintexmid  4621  tfis  4631  tfisi  4635  elomssom  4653  nnregexmid  4669  releq  4757  xpsspw  4787  iss  5005  relcnvtr  5202  iotass  5249  fununi  5342  funcnvuni  5343  funimaexglem  5357  ffoss  5554  ssimaex  5640  tfrlem1  6394  el2oss1o  6529  nnsucsssuc  6578  qsss  6681  phpm  6962  ssfiexmid  6973  findcard2d  6988  findcard2sd  6989  diffifi  6991  isinfinf  6994  fiintim  7028  fisseneq  7031  fidcenumlemrk  7056  fidcenumlemr  7057  sbthlem2  7060  isbth  7069  ctssdclemr  7214  onntri45  7353  tapeq1  7364  elinp  7587  sup3exmid  9030  zfz1isolem1  10985  zfz1iso  10986  fimaxre2  11538  sumeq1  11666  fsum2d  11746  fsumabs  11776  fsumiun  11788  prodeq1f  11863  fprod2d  11934  exmidunben  12797  ctiunct  12811  ssomct  12816  restsspw  13081  lspval  14152  uniopn  14473  fiinopn  14476  fiinbas  14521  baspartn  14522  eltg2  14525  eltg3  14529  topbas  14539  clsval  14583  neival  14615  neiint  14617  neipsm  14626  opnneissb  14627  opnssneib  14628  innei  14635  restbasg  14640  cnpdis  14714  txbas  14730  eltx  14731  neitx  14740  txlm  14751  blssexps  14901  blssex  14902  neibl  14963  metrest  14978  xmettx  14982  tgioo  15026  tgqioo  15027  limcimolemlt  15136  recnprss  15159  dvmptfsum  15197  bj-om  15873  bj-2inf  15874  bj-nntrans  15887  bj-omtrans  15892  subctctexmid  15937  domomsubct  15938  pw1nct  15940