Theorem sseq1 2085

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 2074	. . . 4 ⊢ (B ⊆ A → (A ⊆ C → B ⊆ C))
2		sstr2 2074	. . . 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 2080	. . 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 2050

This theorem is referenced by:  sseq12 2087  sseq1i 2088  sseq1d 2091  psseq1 2138  elpw 2408  elpwg 2409  pwpw0 2473  sssn 2477  sspr 2479  prsspw 2484  pwsnALT 2505  unimax 2536  trss 2694  elssabg 2731  intabs 2738  nnullss 2774  exss 2775  rabsnt 2900  fri 2924  frc 2926  onssmin 3014  releq 3249  iss 3403  fununi 3569  funcnvuni 3570  fssxp 3643  ffoss 3717  ssimaex 3774  isofrlem 3907  f1oweALT 3912  tfrlem1 3917  oawordeu 4195  elpm 4342  pw2en 4452  sbthlem2 4454  sbth 4463  php 4519  unbnn2 4556  fiint 4572  fiintOLD 4573  sucprcreg 4609  unbnnt 4649  tz9.1 4656  setind 4658  rankr1 4684  rankr1id 4707  scott0 4727  bnd2 4734  aceq3lem 4742  ac6lem 4764  zorn2lem7 4804  oncard 4839  carduni 4869  cardaleph 4896  cflem 4917  cflim 4921  cflecard 4924  cfeq0 4926  cfsuc 4927  infxpidmlem2 7554  infxpidmlem3 7555  infxpidmlem7 7559  infxpidmlem8 7560  infmap2lem1 7581  infmap2 7583  uniopnt 7599  eltg2t 7618  tgval3t 7624  topbast 7626  subtop 7643  fctopOLD 7647  cctop 7649  retopbas 7652  iscld 7666  clsval 7674  clsval2 7682  neival 7714  isnei 7715  neiint 7716  neips 7724  opnneissb 7725  opnssneib 7726  innei 7733  islp2 7744  dnsconst 7785  blssex 7851  opnm 7857  blssopn 7864  opnin 7866  neibl 7874  lmbr 7925  bcthlem7 8002  issubg 8112  axgroth3 8774  axgroth4 8775  grothinf 8776  sh 9073  hhsssh 9134  occlt 9177  omls 9241  pjomlt 9264  shintclt 9289  chintclt 9291  spanvalt 9294  shlubt 9349  chnlen0 9363  chsscon3t 9418  chlejb1t 9430  chnlet 9432  spanunt 9463  h1datomt 9500  cmbr4 9539  pjoml2t 9549  pjoml3t 9550  lecmt 9555  osumlem8 9580  osumt 9583  osumcor2 9585  spansncvt 9593  pjcjt2 9632  pjopytht 9660  pjss1co 10086  hstel2t 10141  stjt 10157  stcltr1 10196  mdit 10217  mdbr3 10219  mdbr4 10220  dmdbrt 10221  dmdmdt 10222  dmdbr5 10230  mdsl1 10243  mdslmd1lem3 10249  mdslmd1lem4 10250  mdslmd1 10251  csmdsym 10256  atss 10268  atom1d 10275  superpos 10276  chcv1t 10277  shatomic 10280  shatomistic 10283  hatomistic 10284  chrelat2t 10292  atcvatlem 10307  irred 10316  atcvat4 10319  mdsymlem2 10326  mdsymlem3 10327  mdsymlem6 10330  dmdbr6at 10345  dmdbr7at 10346  infi1 10441  fine 10442  fiiu 10444  ficli 10462  fiv 10470  fiiu2 10473  inposetlem 10475  inposet 10477  iseuctopg 10488  qusp 10541  fillsb 10546  fipfil2 10550  oefil2 10552  fgsb 10555  efilcp 10556  filint2 10557  infi 10559  fgsb2 10560  efilcp2 10561  cnfilca 10562  rcfpfillem3 10565  rcfpfillem4 10566  rcfpfillem5 10567  rcfpfillem6 10568  rcfpfil 10569  limfillem2OLD 10579  ishgrag 10740  hgralem 10741  ispgrag 10750

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 2054  df-ss 2056

Copyright terms: Public domain