Theorem sseq1 2078

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 2067	. . . 4 |- (B (_ A -> (A (_ C -> B (_ C))
2		sstr2 2067	. . . 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 2073	. . 3 |- (B = A <-> (B (_ A /\ A (_ B))
5		bi 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 1475	1 |- (A = B -> (A (_ C <-> B (_ C))

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

This theorem is referenced by:  sseq12 2080  sseq1i 2081  sseq1d 2084  psseq1 2131  elpw 2400  elpwg 2401  pwpw0 2465  sssn 2469  sspr 2471  prsspw 2476  unimax 2527  trss 2684  elssabg 2721  intabs 2728  nnullss 2763  exss 2764  rabsnt 2889  fri 2913  frc 2915  onssmin 3003  releq 3238  iss 3389  fununi 3555  funcnvuni 3556  fssxp 3628  ffoss 3702  ssimaex 3759  isofrlem 3892  f1oweALT 3897  tfrlem1 3902  oawordeu 4179  elpm 4326  pw2en 4432  sbthlem2 4434  sbth 4443  php 4499  unbnn2 4528  fiint 4540  abfii3 4543  abfii4 4544  sucprcreg 4580  unbnnt 4619  tz9.1 4626  setind 4628  rankr1 4654  rankr1id 4677  scott0 4697  bnd2 4704  aceq3lem 4712  ac6lem 4734  zorn2lem7 4774  oncard 4809  carduni 4838  cardaleph 4865  cflem 4885  cflim 4889  cflecard 4892  cfeq0 4894  cfsuc 4895  infxpidmlem2 7504  infxpidmlem3 7505  infxpidmlem7 7509  infxpidmlem8 7510  infmap2lem1 7529  infmap2 7531  uniopnt 7548  eltg2t 7569  tgval3t 7575  topbast 7577  subbas 7594  subbas2 7595  subtop 7596  fctop 7600  cctop 7602  retopbas 7605  iscld 7619  clsval 7627  clsval2 7635  neival 7667  isnei 7668  neiint 7669  neips 7677  opnneissb 7678  opnssneib 7679  innei 7686  islp2 7697  dnsconst 7738  blssex 7806  opnm 7812  blssopn 7819  opnin 7821  neibl 7829  lmbr 7880  bcthlem7 7955  issubg 8068  axgroth3 8718  axgroth4 8719  grothinf 8720  sh 9017  hhsssh 9078  occlt 9121  omls 9184  pjomlt 9207  shintclt 9232  chintclt 9234  spanvalt 9237  shlubt 9292  chnlen0 9306  chsscon3t 9361  chlejb1t 9373  chnlet 9375  spanunt 9406  h1datomt 9445  cmbr4 9484  pjoml2t 9494  pjoml3t 9495  lecmt 9500  osumlem8 9525  osumt 9528  osumcor2 9530  spansncvt 9538  pjcjt2 9577  pjopytht 9605  pjss1co 10029  hstel2t 10084  stjt 10100  stcltr1 10139  mdit 10160  mdbr3 10162  mdbr4 10163  dmdbrt 10164  dmdmdt 10165  mdsl1 10185  mdslmd1lem3 10191  mdslmd1lem4 10192  mdslmd1 10193  csmdsym 10198  atss 10210  atom1d 10217  superpos 10218  chcv1t 10219  shatomic 10222  shatomistic 10225  hatomistic 10226  chrelat2t 10234  atcvatlem 10249  irred 10258  atcvat4 10261  mdsymlem2 10268  mdsymlem3 10269  mdsymlem6 10272  dmdbr6at 10285  infi1 10383  fine 10384  fiiu 10386  ficli 10404  fiv 10410  fiiu2 10413  iseuctopg 10425  qusp 10466  fillsb 10471  fipfil2 10475  oefil2 10477  fgsb 10480  efilcp 10481  filint2 10482  infi 10484  fgsb2 10485  efilcp2 10486  cnfilca 10487  ishgrag 10641  hgralem 10642  ispgrag 10651

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049

Copyright terms: Public domain