Theorem sseq2d 2141

Description: An equality deduction for the subclass relationship.

Hypothesis

Ref	Expression
sseq1d.1	⊢ (φ → A = B)

Assertion

Ref	Expression
sseq2d	⊢ (φ → (C ⊆ A ↔ C ⊆ B))

Proof of Theorem sseq2d

Step	Hyp	Ref	Expression
1		sseq1d.1	. 2 ⊢ (φ → A = B)
2		sseq2 2135	. 2 ⊢ (A = B → (C ⊆ A ↔ C ⊆ B))
3	1, 2	syl 10	1 ⊢ (φ → (C ⊆ A ↔ C ⊆ B))

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

This theorem is referenced by:  sseq12d 2142  sseqtrd 2149  funimass2 3678  fnco 3701  fnssresb 3705  fco 3743  f1ores 3811  foimacnv 3814  resdif 3816  tz6.12-2 3850  ssimaexg 3880  isofrlem 4015  onfununi 4209  oaordi 4316  oawordeulem 4324  oaass 4331  odi 4346  omass 4347  oen0 4349  oelim2 4358  pmvalg 4472  pw2en 4587  sbthlem2 4593  sbth 4602  ssenen 4651  phplem2 4656  pssnn 4681  ssfi 4683  fiint 4703  fodomfi 4709  trcl 4791  r1tr 4800  rankeq0 4842  rankr1id 4843  rankr1b 4845  kmlem5 4915  alephordlem2 5023  alephordi 5024  alephgeom 5032  cardaleph 5035  cardalephex 5036  cflim 5059  isbasisg 7823  tgval 7828  cldval 7876  ntrfval 7877  clsfval 7878  neifval 7924  neiint 7929  lpfval 7952  cncnplem4 7987  opnfval 8067  neibl 8087  lpbl 8090  metequiv 8091  metcnp 8098  lmfval 8136  caufval 8137  metelcls 8176  metcld 8178  cmsss 8208  bcthlem15 8224  bcth 8243  sspval 8636  hsupunss 9589  spanss2 9590  orthin 9646  chssoc 9695  chsscon3 9699  chsscon1 9700  h1datom 9781  pjoml6i 9808  osumlem8 9863  osum 9866  spansncv 9876  pjcjt2 9915  pjopyth 9943  hstel2 10427  hstle 10438  stj 10443  dmdbr5 10516  mdslmd1lem1 10533  atord 10597  irredlem4 10602  atcvat4i 10606  mdsymlem2 10613  mdsymlem3 10614  mdsymlem8 10619  mdsymi 10620  ghomfo 10676  abfi2 10853  inpc 10867  stoig 11064  isfil 11071  oefil2 11079  fgsb 11082  fgsb2 11086  topsinind 11136  issubcat 11299  fictblem 11422  cnpnei 11472  subcld 11480  subntr 11482  compsublem 11487  compsub 11488  cptclsscpt 11489  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  connsub 11502  reconnlem1 11507  ivthALT 11515  isfne 11541  locfincf 11577  neibastop1 11579  neibastop2lem4 11583  topmeet 11587  fbasssin 11625  fbssint 11626  fgfil 11638  fbfgss 11640  filrn 11643  neifg 11644  ufileu 11658  filufint 11659  ufinffr 11663  cnpfillim 11686  elfilmap 11690  fmfnfmlem4 11703  flimfnfcls 11727  fcluscomplem 11732  tailfb 11762  raleqfn 11790  fipreima 11848  metsstop 11909  sstotbnd 11992  ismtyhmeolem 12006  ismtyres 12010  heiborlem20 12030  heiborlem21 12031  heiborlem23 12033  heiborlem38 12048  heiborlem42 12052  rrntotbnd 12078  rrnheibor 12079  ishgrag 12195  hgralem 12196  ispgrag 12205

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