Theorem sseq1 3020

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 3014	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3006	. . . 4 |- ( B C_ A -> ( A C_ C -> B C_ C ) )
3	2	adantl 271	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C -> B C_ C ) )
4		sstr2 3006	. . . 4 |- ( A C_ B -> ( B C_ C -> A C_ C ) )
5	4	adantr 270	. . 3 |- ( ( A C_ B /\ B C_ A ) -> ( B C_ C -> A C_ C ) )
6	3, 5	impbid 127	. 2 |- ( ( A C_ B /\ B C_ A ) -> ( A C_ C <-> B C_ C ) )
7	1, 6	sylbi 119	1 |- ( A = B -> ( A C_ C <-> B C_ C ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   = wceq 1284   C_ wss 2973

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-11 1437  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-in 2979  df-ss 2986

This theorem is referenced by:  sseq12  3022  sseq1i  3023  sseq1d  3026  nssne2  3056  sbss  3349  pwjust  3383  elpw  3388  elpwg  3390  sssnr  3545  ssprr  3548  sstpr  3549  unimax  3635  trss  3884  elssabg  3923  bnd2  3947  mss  3981  exss  3982  frforeq2  4100  ordtri2orexmid  4266  ontr2exmid  4268  onsucsssucexmid  4270  reg2exmidlema  4277  sucprcreg  4292  ordtri2or2exmid  4314  onintexmid  4315  tfis  4324  tfisi  4328  elnn  4346  nnregexmid  4360  releq  4440  xpsspw  4468  iss  4674  relcnvtr  4860  iotass  4904  fununi  4987  funcnvuni  4988  funimaexglem  5002  ffoss  5178  ssimaex  5255  tfrlem1  5946  nnsucsssuc  6094  qsss  6188  phpm  6351  ssfiexmid  6361  findcard2d  6375  findcard2sd  6376  diffifi  6378  elinp  6664  fimaxre2  10109  sumeq1  10192  bj-om  10732  bj-2inf  10733  bj-nntrans  10746  bj-omtrans  10751