Theorem sseq1 3115

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 3107	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3099	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 275	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3099	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 274	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6	3, 5	impbid 128	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7	1, 6	sylbi 120	1 |- ( A = B -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   = wceq 1331   C_ wss 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  sseq12  3117  sseq1i  3118  sseq1d  3121  nssne2  3151  sbss  3466  pwjust  3506  elpw  3511  elpwg  3513  sssnr  3675  ssprr  3678  sstpr  3679  unimax  3765  trss  4030  elssabg  4068  bnd2  4092  exmidexmid  4115  exmidsssn  4120  exmidsssnc  4121  mss  4143  exss  4144  frforeq2  4262  ordtri2orexmid  4433  ontr2exmid  4435  onsucsssucexmid  4437  reg2exmidlema  4444  sucprcreg  4459  ordtri2or2exmid  4481  onintexmid  4482  tfis  4492  tfisi  4496  elnn  4514  nnregexmid  4529  releq  4616  xpsspw  4646  iss  4860  relcnvtr  5053  iotass  5100  fununi  5186  funcnvuni  5187  funimaexglem  5201  ffoss  5392  ssimaex  5475  tfrlem1  6198  nnsucsssuc  6381  qsss  6481  phpm  6752  ssfiexmid  6763  findcard2d  6778  findcard2sd  6779  diffifi  6781  isinfinf  6784  fiintim  6810  fisseneq  6813  fidcenumlemrk  6835  fidcenumlemr  6836  sbthlem2  6839  isbth  6848  ctssdclemr  6990  elinp  7275  sup3exmid  8708  zfz1isolem1  10576  zfz1iso  10577  fimaxre2  10991  sumeq1  11117  fsum2d  11197  fsumabs  11227  fsumiun  11239  prodeq1f  11314  exmidunben  11928  ctiunct  11942  restsspw  12119  uniopn  12157  fiinopn  12160  fiinbas  12205  baspartn  12206  eltg2  12211  eltg3  12215  topbas  12225  clsval  12269  neival  12301  neiint  12303  neipsm  12312  opnneissb  12313  opnssneib  12314  innei  12321  restbasg  12326  cnpdis  12400  txbas  12416  eltx  12417  neitx  12426  txlm  12437  blssexps  12587  blssex  12588  neibl  12649  metrest  12664  xmettx  12668  tgioo  12704  tgqioo  12705  limcimolemlt  12791  recnprss  12814  bj-om  13124  bj-2inf  13125  bj-nntrans  13138  bj-omtrans  13143  el2oss1o  13177  exmid1stab  13184  subctctexmid  13185