Theorem sseq2i 2138

Description: An equality inference for the subclass relationship.

Hypothesis

Ref	Expression
sseq1i.1	⊢ A = B

Assertion

Ref	Expression
sseq2i	⊢ (C ⊆ A ↔ C ⊆ B)

Proof of Theorem sseq2i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 ⊢ A = B
2		sseq2 2135	. 2 ⊢ (A = B → (C ⊆ A ↔ C ⊆ B))
3	1, 2	ax-mp 7	1 ⊢ (C ⊆ A ↔ C ⊆ B)

Syntax hints:   ↔ wb 144   = wceq 992   ⊆ wss 2099

This theorem is referenced by:  sseqtri 2145  syl6ss 2159  abss 2169  ssrab 2177  ssindif0 2375  difcom 2399  sspr 2540  iunpwss 2691  elpwun 3134  dffun2 3631  ssimaex 3879  rankeq0 4842  iscard2 5004  alephislim 5033  cardaleph 5035  ssxr 5694  nnwo 6585  subtop 7858  chsscon1i 9661  hatomistici 10570  irredlem4 10602  atabs2i 10611  mdsymlem1 10612  mdsymlem3 10614  mdsymlem6 10617  mdsymlem8 10619  dmdbr5ati 10631  mapdiscn 11014  dtopcl 11107  stfincomp 11122  usinuniop 11128  clindistop 11131  altretoplem1 11142  idsubc 11305  elsubsp 11477  subsubtop 11479  subcld 11480  subcls 11481  subntr 11482  cnsubsp 11483  cnsubsp2 11484  compsublem 11487  compsub 11488  cncomp 11494  connsub 11502  subtopmetlem 11505  reconn 11512  2ndcctbss 11539  neibastop2lem4 11583  ist1-3 11604  filssufillem 11655  filufint 11659  subspabs 11903  cnimass 11949  cnres 11950  cnres2 11951  cnss 11953  txsubsp 11983  heiborlem8 12018  heiborlem11 12021  heiborlem13 12023  heiborlem15 12025  heiborlem38 12048  heiborlem42 12052

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105

Copyright terms: Public domain