Theorem sseq1 3247

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 3239	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3231	. . . 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 3231	. . . 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 1395   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sseq12  3249  sseq1i  3250  sseq1d  3253  nssne2  3283  sbss  3599  pwjust  3650  elpw  3655  elpwg  3657  sssnr  3831  ssprr  3834  sstpr  3835  unimax  3922  trss  4191  elssabg  4232  bnd2  4257  exmidexmid  4280  exmidsssn  4286  exmidsssnc  4287  exmid1stab  4292  mss  4312  exss  4313  frforeq2  4436  ordtri2orexmid  4615  ontr2exmid  4617  onsucsssucexmid  4619  reg2exmidlema  4626  sucprcreg  4641  ordtri2or2exmid  4663  ontri2orexmidim  4664  onintexmid  4665  tfis  4675  tfisi  4679  elomssom  4697  nnregexmid  4713  releq  4801  xpsspw  4831  iss  5051  relcnvtr  5248  iotass  5296  fununi  5389  funcnvuni  5390  funimaexglem  5404  ffoss  5606  ssimaex  5697  tfrlem1  6460  el2oss1o  6597  nnsucsssuc  6646  qsss  6749  phpm  7035  ssfiexmid  7046  findcard2d  7061  findcard2sd  7062  diffifi  7064  isinfinf  7067  fiintim  7104  fisseneq  7107  fidcenumlemrk  7132  fidcenumlemr  7133  sbthlem2  7136  isbth  7145  ctssdclemr  7290  onntri45  7437  tapeq1  7449  elinp  7672  sup3exmid  9115  zfz1isolem1  11075  zfz1iso  11076  fimaxre2  11753  sumeq1  11881  fsum2d  11961  fsumabs  11991  fsumiun  12003  prodeq1f  12078  fprod2d  12149  exmidunben  13012  ctiunct  13026  ssomct  13031  restsspw  13297  lspval  14369  uniopn  14690  fiinopn  14693  fiinbas  14738  baspartn  14739  eltg2  14742  eltg3  14746  topbas  14756  clsval  14800  neival  14832  neiint  14834  neipsm  14843  opnneissb  14844  opnssneib  14845  innei  14852  restbasg  14857  cnpdis  14931  txbas  14947  eltx  14948  neitx  14957  txlm  14968  blssexps  15118  blssex  15119  neibl  15180  metrest  15195  xmettx  15199  tgioo  15243  tgqioo  15244  limcimolemlt  15353  recnprss  15376  dvmptfsum  15414  lpvtx  15894  bj-om  16355  bj-2inf  16356  bj-nntrans  16369  bj-omtrans  16374  subctctexmid  16425  domomsubct  16426  pw1nct  16428