Theorem sseq1 2082

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 2071	. . . 4 |- (B (_ A -> (A (_ C -> B (_ C))
2		sstr2 2071	. . . 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 2077	. . 3 |- (B = A <-> (B (_ A /\ A (_ B))
5		dfbi2 514	. . 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 1478	1 |- (A = B -> (A (_ C <-> B (_ C))

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

This theorem is referenced by:  sseq12 2084  sseq1i 2085  sseq1d 2088  psseq1 2135  elpw 2404  elpwg 2405  pwpw0 2469  sssn 2473  sspr 2475  prsspw 2480  pwsnALT 2501  unimax 2532  trss 2689  elssabg 2726  intabs 2733  nnullss 2768  exss 2769  rabsnt 2894  fri 2918  frc 2920  onssmin 3008  releq 3243  iss 3397  fununi 3563  funcnvuni 3564  fssxp 3637  ffoss 3711  ssimaex 3768  isofrlem 3901  f1oweALT 3906  tfrlem1 3911  oawordeu 4189  elpm 4336  pw2en 4446  sbthlem2 4448  sbth 4457  php 4513  unbnn2 4545  fiint 4559  fiintOLD 4560  abfii3OLD 4563  abfii4OLD 4564  sucprcreg 4600  unbnnt 4639  tz9.1 4646  setind 4648  rankr1 4674  rankr1id 4697  scott0 4717  bnd2 4724  aceq3lem 4732  ac6lem 4754  zorn2lem7 4794  oncard 4829  carduni 4858  cardaleph 4885  cflem 4905  cflim 4909  cflecard 4912  cfeq0 4914  cfsuc 4915  infxpidmlem2 7553  infxpidmlem3 7554  infxpidmlem7 7558  infxpidmlem8 7559  infmap2lem1 7579  infmap2 7581  uniopnt 7598  eltg2t 7619  tgval3t 7625  topbast 7627  subbasOLD 7644  subbas2OLD 7645  subtop 7646  fctopOLD 7650  cctop 7652  retopbas 7655  iscld 7669  clsval 7677  clsval2 7685  neival 7717  isnei 7718  neiint 7719  neips 7727  opnneissb 7728  opnssneib 7729  innei 7736  islp2 7747  dnsconst 7788  blssex 7854  opnm 7860  blssopn 7867  opnin 7869  neibl 7877  lmbr 7928  bcthlem7 8005  issubg 8116  axgroth3 8779  axgroth4 8780  grothinf 8781  sh 9078  hhsssh 9139  occlt 9182  omls 9246  pjomlt 9269  shintclt 9294  chintclt 9296  spanvalt 9299  shlubt 9354  chnlen0 9368  chsscon3t 9423  chlejb1t 9435  chnlet 9437  spanunt 9468  h1datomt 9505  cmbr4 9544  pjoml2t 9554  pjoml3t 9555  lecmt 9560  osumlem8 9585  osumt 9588  osumcor2 9590  spansncvt 9598  pjcjt2 9637  pjopytht 9665  pjss1co 10091  hstel2t 10146  stjt 10162  stcltr1 10201  mdit 10222  mdbr3 10224  mdbr4 10225  dmdbrt 10226  dmdmdt 10227  dmdbr5 10235  mdsl1 10248  mdslmd1lem3 10254  mdslmd1lem4 10255  mdslmd1 10256  csmdsym 10261  atss 10273  atom1d 10280  superpos 10281  chcv1t 10282  shatomic 10285  shatomistic 10288  hatomistic 10289  chrelat2t 10297  atcvatlem 10312  irred 10321  atcvat4 10324  mdsymlem2 10331  mdsymlem3 10332  mdsymlem6 10335  dmdbr6at 10350  dmdbr7at 10351  infi1 10447  infi1OLD 10448  fine 10449  fineOLD 10450  fiiu 10453  fiiuOLD 10454  ficli 10472  ficliOLD 10473  fiv 10482  fivOLD 10483  fiiu2 10488  fiiu2OLD 10489  iseuctopg 10502  qusp 10555  fillsb 10560  fipfil2 10564  fipfil2OLD 10565  oefil2 10567  fgsb 10570  fgsbOLD 10571  efilcp 10572  efilcpOLD 10573  filint2 10574  filint2OLD 10575  infi 10578  infiOLD 10579  fgsb2 10580  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  rcfpfillem3 10589  rcfpfillem3OLD 10590  rcfpfillem4 10591  rcfpfillem4OLD 10592  rcfpfillem5 10593  rcfpfillem5OLD 10594  rcfpfillem6 10595  rcfpfillem6OLD 10596  rcfpfil 10597  rcfpfilOLD 10598  limfillem2OLD 10608  ishgrag 10769  hgralem 10770  ispgrag 10779

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053

Copyright terms: Public domain