Theorem sseq1 3271

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 3263	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
2		sstr2 3255	. . . 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 3255	. . . 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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   = wceq 1402   C_ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  sseq12  3273  sseq1i  3274  sseq1d  3277  nssne2  3307  vvin  3569  sbss  3635  pwjust  3689  elpw  3694  elpwg  3696  sssnr  3878  ssprr  3881  sstpr  3882  unimax  3969  trss  4238  elssabg  4284  bnd2  4310  exmidexmid  4333  exmidsssn  4339  exmidsssnc  4340  exmid1stab  4345  mss  4366  exss  4367  frforeq2  4490  ordtri2orexmid  4670  ontr2exmid  4672  onsucsssucexmid  4674  reg2exmidlema  4681  sucprcreg  4696  ordtri2or2exmid  4718  ontri2orexmidim  4719  onintexmid  4720  tfis  4730  tfisi  4734  elomssom  4752  nnregexmid  4768  releq  4857  xpsspw  4887  iss  5109  relcnvtr  5307  iotass  5355  fununi  5449  funcnvuni  5450  funimaexglem  5464  ffoss  5672  ssimaex  5764  tfrlem1  6579  el2oss1o  6716  nnsucsssuc  6765  qsss  6868  phpm  7167  ssfiexmid  7178  ssfiexmidt  7180  findcard2d  7195  findcard2sd  7196  diffifi  7198  isinfinf  7201  fiintim  7238  fisseneq  7242  fidcenumlemrk  7271  fidcenumlemr  7272  sbthlem2  7275  isbth  7284  ctssdclemr  7452  onntri45  7600  papeq1  7609  tapeq1  7618  elinp  7841  sup3exmid  9289  zfz1isolem1  11306  zfz1iso  11307  fimaxre2  12008  sumeq1  12137  fsum2d  12218  fsumabs  12248  fsumiun  12260  prodeq1f  12335  fprod2d  12406  exmidunben  13366  ctiunct  13380  ssomct  13385  restsspw  13652  lspval  14776  aspval  15064  uniopn  15151  fiinopn  15154  fiinbas  15199  baspartn  15200  eltg2  15203  eltg3  15207  topbas  15217  clsval  15261  neival  15293  neiint  15295  neipsm  15304  opnneissb  15305  opnssneib  15306  innei  15313  restbasg  15318  cnpdis  15392  txbas  15408  eltx  15409  neitx  15418  txlm  15429  blssexps  15579  blssex  15580  neibl  15641  metrest  15656  xmettx  15660  tgioo  15704  tgqioo  15705  limcimolemlt  15814  recnprss  15837  dvmptfsum  15875  lpvtx  16418  issubgr2  16597  subgrprop2  16599  egrsubgr  16602  0uhgrsubgr  16604  bj-om  17061  bj-2inf  17062  bj-nntrans  17075  bj-omtrans  17080  subctctexmid  17128  domomsubct  17129  pw1nct  17131