Theorem sseq2 2639

Description: Equality theorem for the subclass relationship.

Assertion

Ref	Expression
sseq2	|- (A = B -> (C C_ A <-> C C_ B))

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 2623	. . . 4 |- (C C_ A -> (A C_ B -> C C_ B))
2	1	com12 14	. . 3 |- (A C_ B -> (C C_ A -> C C_ B))
3		sstr2 2623	. . . 4 |- (C C_ B -> (B C_ A -> C C_ A))
4	3	com12 14	. . 3 |- (B C_ A -> (C C_ B -> C C_ A))
5	2, 4	anim12i 360	. 2 |- ((A C_ B /\ B C_ A) -> ((C C_ A -> C C_ B) /\ (C C_ B -> C C_ A)))
6		eqss 2631	. 2 |- (A = B <-> (A C_ B /\ B C_ A))
7		dfbi2 572	. 2 |- ((C C_ A <-> C C_ B) <-> ((C C_ A -> C C_ B) /\ (C C_ B -> C C_ A)))
8	5, 6, 7	3imtr4i 236	1 |- (A = B -> (C C_ A <-> C C_ B))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   C_ wss 2593

This theorem is referenced by:  sseq12 2640  sseq2i 2642  sseq2d 2645  eqimssOLD 2666  psseq2 2698  sseq0 2903  sseq0OLD 2904  un00 2907  disjpss 2924  pweq 3036  ssuniOLD 3202  ssintab 3233  ssintabOLD 3234  ssintub 3235  intmin 3237  intminOLD 3238  treq 3417  ssexg 3457  intabs 3469  ordunidif 3712  ordssun 3769  iunpw 3858  tfindsg 3944  limomss 3956  findsg 3980  unixp0 4423  fununi 4481  funcnvuni 4482  feq3 4553  feq23OLD 4555  ssimaexg 4730  onfununi 5116  oawordeu 5237  oawordexr 5238  ereq 5324  domeng 5439  undom 5497  ac6sfi 5509  sbthlem4 5513  sbthlem5 5514  mapdom2lem 5587  php3 5609  abfii4 5654  inf3lema 5715  tz9.1 5753  scottex 5846  omsubinit 5890  aceq3 5895  ac7g 5911  cardlim 6003  isinfcard 6035  alephval3 6051  cflem 6053  cfval 6054  cflecard 6060  cfsuc 6063  infxpidmlem7 8827  infxpidmlem11 8831  istopg 8865  basis2 8884  eltg2 8889  tgss2 8907  basgen2 8909  bastop1 8912  ntrval 8952  clsval 8953  clscld 8959  clsval2 8961  ntrcls0 8983  isnei 8994  neiint 8995  neips 9003  opnneissb 9004  opnssneib 9005  innei 9012  islp2 9023  cnpimaex 9041  cnpnei 9043  isopn 9136  metcnp 9165  tgioo 9193  resgrprn 9403  issubg 9425  axgroth6 10137  avril1 10142  fiv 10212  fiuni 10219  fillsb 10270  fbssint 10279  fbfgss 10288  extbas1 10291  limfil 10297  neifil 10302  elfilmap3 10314  flimfneii 10320  flimopn 10321  fbaslim 10322  cncomp 10331  omlsi 10879  pjoml 10902  ococin 10930  spanval 10932  hsupval2 10933  spancl 10937  chsupsn 10945  shlub 10987  shsumval2i 10993  shs00i 11006  chj00i 11043  chsscon3 11056  chlejb1 11068  chnle 11070  pjoml2 11187  pjoml3 11188  lecm 11193  stcltr1i 11846  mdbr 11866  dmdmd 11872  dmdi 11874  dmdbr3 11877  dmdbr4 11878  mdsl1i 11893  mdslmd1lem3 11899  mdslmd1lem4 11900  csmdsymi 11906  hatomic 11932  chrelat2 11942  atord 11960  atcvat4i 11969  bnj1264 13022  bnj1287 13477  bnj1288 13478  bnj1290 13479  bnj1291 13480  bnj1462 13546  frxp 13951  wfrlem1 13957  wfrlem4 13960  wfrlem15 13971  axfelem16 14046  altopth1sn 14090  sqpeq 14383  r1subsuc 14439  prl 14512  prjmapcp2 14515  inposetlem 14618  inposet 14620  dominc 14622  domncnt 14624  svs2 14829  unint2t 14866  intfmu2 14867  mapdiscnlem 14870  osneisi 14875  fgsb 14921  efilcp 14922  fgsb2 14925  efilcp2 14926  fbaslim2 14936  limfillem1 14938  limfillem2 14939  iscnp3 14946  bwt2 14960  topsinind 14967  lvsovso 15038  isalg 15068  algi 15074  dualcat2lem 15129  dualded2lem 15130  dualalg 15131  taralt 15211  tarval 15212  tarvalg 15213  tarval1 15214  tarval1g 15215  bpmp 15251  vtarsuelt 15272  partarelt1 15273  fictb 15371  finsschain 15373  omsubinitOLD 15399  cncls 15419  cnntr 15420  subcls 15424  uncomp 15433  hscptsscld 15434  compfipin0 15436  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  alexsub 15441  2ndcsb 15476  2ndcctbss 15478  fnessex 15484  ssref 15492  refref 15494  fnessref 15503  refssfne 15504  comppfsc 15517  neibastop1 15518  neibastop2lem1 15519  neibastop2lem2 15520  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  topjoin 15527  fnemeet1 15528  fnemeet2 15529  fnejoin2 15531  isnrm2 15552  opnfbas 15557  fgmin 15558  neifg 15559  supfil 15560  isufil2 15565  ufilmax 15568  filssufillem 15570  filssufil 15571  ufileu 15573  filufint 15574  fixufil 15576  ufilen 15579  limfilcf 15587  fmfnfmlem4 15597  fmfnfm 15598  isfclus 15606  fcluscf 15612  fclsfnflim 15614  flimfnfcls 15615  fcluscnplem 15617  fcluscnp 15618  fcluscomplem 15620  fcluscomp 15621  filnetlem1 15640  filnetlem2 15641  filnetlem3 15642  filnetlem4 15643  filnetlem5 15644  txmet 15925  sstotbnd 15936  totbndss 15937  ismtyhmeolem 15950  heiborlem13 15967  unichnidl 16179  ispridl 16182  maxidlmax 16191  igenval 16209  igenidl 16211  igenmin 16212  igenval2 16214

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-in 2603  df-ss 2605

Copyright terms: Public domain