Theorem sseq1 3179

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 3171	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3163	. . . 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 3163	. . . 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 3130

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 3136  df-ss 3143

This theorem is referenced by:  sseq12  3181  sseq1i  3182  sseq1d  3185  nssne2  3215  sbss  3532  pwjust  3577  elpw  3582  elpwg  3584  sssnr  3754  ssprr  3757  sstpr  3758  unimax  3844  trss  4111  elssabg  4149  bnd2  4174  exmidexmid  4197  exmidsssn  4203  exmidsssnc  4204  exmid1stab  4209  mss  4227  exss  4228  frforeq2  4346  ordtri2orexmid  4523  ontr2exmid  4525  onsucsssucexmid  4527  reg2exmidlema  4534  sucprcreg  4549  ordtri2or2exmid  4571  ontri2orexmidim  4572  onintexmid  4573  tfis  4583  tfisi  4587  elomssom  4605  nnregexmid  4621  releq  4709  xpsspw  4739  iss  4954  relcnvtr  5149  iotass  5196  fununi  5285  funcnvuni  5286  funimaexglem  5300  ffoss  5494  ssimaex  5578  tfrlem1  6309  el2oss1o  6444  nnsucsssuc  6493  qsss  6594  phpm  6865  ssfiexmid  6876  findcard2d  6891  findcard2sd  6892  diffifi  6894  isinfinf  6897  fiintim  6928  fisseneq  6931  fidcenumlemrk  6953  fidcenumlemr  6954  sbthlem2  6957  isbth  6966  ctssdclemr  7111  onntri45  7240  tapeq1  7251  elinp  7473  sup3exmid  8914  zfz1isolem1  10820  zfz1iso  10821  fimaxre2  11235  sumeq1  11363  fsum2d  11443  fsumabs  11473  fsumiun  11485  prodeq1f  11560  fprod2d  11631  exmidunben  12427  ctiunct  12441  ssomct  12446  restsspw  12698  uniopn  13504  fiinopn  13507  fiinbas  13552  baspartn  13553  eltg2  13556  eltg3  13560  topbas  13570  clsval  13614  neival  13646  neiint  13648  neipsm  13657  opnneissb  13658  opnssneib  13659  innei  13666  restbasg  13671  cnpdis  13745  txbas  13761  eltx  13762  neitx  13771  txlm  13782  blssexps  13932  blssex  13933  neibl  13994  metrest  14009  xmettx  14013  tgioo  14049  tgqioo  14050  limcimolemlt  14136  recnprss  14159  bj-om  14692  bj-2inf  14693  bj-nntrans  14706  bj-omtrans  14711  subctctexmid  14753  pw1nct  14755