Theorem sseq1 2086

Description: Equality theorem for subclasses.

Assertion

Ref	Expression
sseq1	|- (A = B -> (A (_ C <-> B (_ C))

Proof of Theorem sseq1

Step	Hyp	Ref	Expression
1		sstr2 2075	. . . 4 |- (B (_ A -> (A (_ C -> B (_ C))
2		sstr2 2075	. . . 4 |- (A (_ B -> (B (_ C -> A (_ C))
3	1, 2	anim12i 333	. . 3 |- ((B (_ A /\ A (_ B) -> ((A (_ C -> B (_ C) /\ (B (_ C -> A (_ C)))
4		eqss 2081	. . 3 |- (B = A <-> (B (_ A /\ A (_ B))
5		dfbi2 516	. . 3 |- ((A (_ C <-> B (_ C) <-> ((A (_ C -> B (_ C) /\ (B (_ C -> A (_ C)))
6	3, 4, 5	3imtr4 219	. 2 |- (B = A -> (A (_ C <-> B (_ C))
7	6	eqcoms 1481	1 |- (A = B -> (A (_ C <-> B (_ C))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 958   (_ wss 2051

This theorem is referenced by:  sseq12 2088  sseq1i 2089  sseq1d 2092  psseq1 2139  elpw 2409  elpwg 2410  pwpw0 2474  sssn 2478  sspr 2480  prsspw 2485  pwsnALT 2506  unimax 2537  trss 2695  elssabg 2732  intabs 2739  nnullss 2775  exss 2776  rabsnt 2901  fri 2925  frc 2927  onssmin 3015  releq 3250  iss 3404  fununi 3570  funcnvuni 3571  fssxp 3644  ffoss 3718  ssimaex 3775  isofrlem 3908  f1oweALT 3913  tfrlem1 3918  oawordeu 4196  elpm 4343  pw2en 4453  sbthlem2 4455  sbth 4464  php 4520  unbnn2 4558  fiint 4576  fiintOLD 4577  abfii3 4581  sucprcreg 4616  unbnnt 4656  tz9.1 4663  setind 4665  rankr1 4691  rankr1id 4714  scott0 4734  bnd2 4741  aceq3lem 4749  ac6lem 4771  zorn2lem7 4811  oncard 4846  carduni 4876  cardaleph 4903  cflem 4924  cflim 4928  cflecard 4931  cfeq0 4933  cfsuc 4934  infxpidmlem2 7561  infxpidmlem3 7562  infxpidmlem7 7566  infxpidmlem8 7567  infmap2lem1 7588  infmap2 7590  uniopnt 7606  eltg2t 7625  tgval3t 7631  topbast 7633  subtop 7650  fctopOLD 7654  cctop 7656  retopbas 7659  iscld 7673  clsval 7681  clsval2 7689  neival 7721  isnei 7722  neiint 7723  neips 7731  opnneissb 7732  opnssneib 7733  innei 7740  islp2 7751  dnsconst 7792  blssex 7858  opnm 7864  blssopn 7871  opnin 7873  neibl 7881  lmbr 7932  bcthlem7 8009  issubg 8119  axgroth3 8781  axgroth4 8782  grothinf 8783  sh 9080  hhsssh 9141  occlt 9184  omls 9248  pjomlt 9271  shintclt 9296  chintclt 9298  spanvalt 9301  shlubt 9356  chnlen0 9370  chsscon3t 9425  chlejb1t 9437  chnlet 9439  spanunt 9470  h1datomt 9507  cmbr4 9546  pjoml2t 9556  pjoml3t 9557  lecmt 9562  osumlem8 9587  osumt 9590  osumcor2 9592  spansncvt 9600  pjcjt2 9639  pjopytht 9667  pjss1co 10093  hstel2t 10149  stjt 10165  stcltr1 10204  mdit 10225  mdbr3 10227  mdbr4 10228  dmdbrt 10229  dmdmdt 10230  dmdbr5 10238  mdsl1 10251  mdslmd1lem3 10257  mdslmd1lem4 10258  mdslmd1 10259  csmdsym 10264  atss 10276  atom1d 10283  superpos 10284  chcv1t 10285  shatomic 10288  shatomistic 10291  hatomistic 10292  chrelat2t 10300  atcvatlem 10315  irred 10324  atcvat4 10327  mdsymlem2 10334  mdsymlem3 10335  mdsymlem6 10338  dmdbr6at 10353  dmdbr7at 10354  infi1 10449  fine 10450  fiiu 10452  ficli 10470  fiv 10478  fiiu2 10481  inposetlem 10483  inposet 10485  iseuctopg 10496  qusp 10549  fillsb 10554  fipfil2 10558  oefil2 10560  fgsb 10563  efilcp 10564  filint2 10565  infi 10567  fgsb2 10568  efilcp2 10569  cnfilca 10570  rcfpfillem3 10573  rcfpfillem4 10574  rcfpfillem5 10575  rcfpfillem6 10576  rcfpfil 10577  limfillem2OLD 10587  ishgrag 10748  hgralem 10749  ispgrag 10758

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2055  df-ss 2057

Copyright terms: Public domain