Theorem sseq1 3178

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 3170	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3162	. . . 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 3162	. . . 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 1353   C_ wss 3129

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142

This theorem is referenced by:  sseq12  3180  sseq1i  3181  sseq1d  3184  nssne2  3214  sbss  3531  pwjust  3576  elpw  3581  elpwg  3583  sssnr  3752  ssprr  3755  sstpr  3756  unimax  3842  trss  4108  elssabg  4146  bnd2  4171  exmidexmid  4194  exmidsssn  4200  exmidsssnc  4201  exmid1stab  4206  mss  4224  exss  4225  frforeq2  4343  ordtri2orexmid  4520  ontr2exmid  4522  onsucsssucexmid  4524  reg2exmidlema  4531  sucprcreg  4546  ordtri2or2exmid  4568  ontri2orexmidim  4569  onintexmid  4570  tfis  4580  tfisi  4584  elomssom  4602  nnregexmid  4618  releq  4706  xpsspw  4736  iss  4950  relcnvtr  5145  iotass  5192  fununi  5281  funcnvuni  5282  funimaexglem  5296  ffoss  5490  ssimaex  5574  tfrlem1  6304  el2oss1o  6439  nnsucsssuc  6488  qsss  6589  phpm  6860  ssfiexmid  6871  findcard2d  6886  findcard2sd  6887  diffifi  6889  isinfinf  6892  fiintim  6923  fisseneq  6926  fidcenumlemrk  6948  fidcenumlemr  6949  sbthlem2  6952  isbth  6961  ctssdclemr  7106  onntri45  7235  tapeq1  7246  elinp  7468  sup3exmid  8908  zfz1isolem1  10811  zfz1iso  10812  fimaxre2  11226  sumeq1  11354  fsum2d  11434  fsumabs  11464  fsumiun  11476  prodeq1f  11551  fprod2d  11622  exmidunben  12417  ctiunct  12431  ssomct  12436  restsspw  12684  uniopn  13281  fiinopn  13284  fiinbas  13329  baspartn  13330  eltg2  13335  eltg3  13339  topbas  13349  clsval  13393  neival  13425  neiint  13427  neipsm  13436  opnneissb  13437  opnssneib  13438  innei  13445  restbasg  13450  cnpdis  13524  txbas  13540  eltx  13541  neitx  13550  txlm  13561  blssexps  13711  blssex  13712  neibl  13773  metrest  13788  xmettx  13792  tgioo  13828  tgqioo  13829  limcimolemlt  13915  recnprss  13938  bj-om  14460  bj-2inf  14461  bj-nntrans  14474  bj-omtrans  14479  subctctexmid  14521  pw1nct  14523