Theorem sseq2 2086

Description: Equality theorem for the subclass relationship.

Assertion

Ref	Expression
sseq2	⊢ (A = B → (C ⊆ A ↔ C ⊆ B))

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 2074	. . . 4 ⊢ (C ⊆ A → (A ⊆ B → C ⊆ B))
2	1	com12 11	. . 3 ⊢ (A ⊆ B → (C ⊆ A → C ⊆ B))
3		sstr2 2074	. . . 4 ⊢ (C ⊆ B → (B ⊆ A → C ⊆ A))
4	3	com12 11	. . 3 ⊢ (B ⊆ A → (C ⊆ B → C ⊆ A))
5	2, 4	anim12i 333	. 2 ⊢ ((A ⊆ B ⋀ B ⊆ A) → ((C ⊆ A → C ⊆ B) ⋀ (C ⊆ B → C ⊆ A)))
6		eqss 2080	. 2 ⊢ (A = B ↔ (A ⊆ B ⋀ B ⊆ A))
7		dfbi2 516	. 2 ⊢ ((C ⊆ A ↔ C ⊆ B) ↔ ((C ⊆ A → C ⊆ B) ⋀ (C ⊆ B → C ⊆ A)))
8	5, 6, 7	3imtr4 219	1 ⊢ (A = B → (C ⊆ A ↔ C ⊆ B))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   = wceq 958   ⊆ wss 2050

This theorem is referenced by:  sseq12 2087  sseq2i 2089  sseq2d 2092  eqimss 2112  psseq2 2139  sseq0 2308  un00 2310  disjpss 2323  pweq 2407  ssuni 2526  ssintab 2554  ssintub 2555  intmin 2557  treq 2691  ssexg 2726  intabs 2738  iunpw 2920  ordunidif 3011  ordssun 3085  limomss 3143  findsg 3163  tfindsg 3168  unixp0 3524  fununi 3569  funcnvuni 3570  feq3 3628  feq23 3629  ssimaexg 3775  oawordeu 4195  oawordexr 4196  ereq 4273  domeng 4386  undom 4444  sbthlem4 4456  sbthlem5 4457  mapdom2lem 4499  php3 4521  php3OLD 4522  inf3lema 4618  tz9.1 4656  scottex 4726  aceq3 4743  ac7g 4759  cardlim 4862  isinfcard 4898  alephval3 4914  cflem 4917  cfval 4918  cflecard 4924  cfsuc 4927  infxpidmlem7 7559  infxpidmlem11 7563  istopg 7598  basis2t 7614  eltg2t 7618  tgss2t 7636  basgen2t 7638  bastop 7641  ntrval 7673  clsval 7674  clscld 7680  clsval2 7682  ntrcls0 7704  isnei 7715  neiint 7716  neips 7724  opnneissb 7725  opnssneib 7726  innei 7733  islp2 7744  cnpimaex 7762  isopn 7856  metcnp 7884  tgioo 7912  resgrprn 8091  issubg 8112  avril1 8779  omls 9241  pjomlt 9264  ococint 9292  spanvalt 9294  hsupval2t 9295  spanclt 9299  chsupsn 9307  shlubt 9349  shsumval2 9355  shs00 9368  chj00 9405  chsscon3t 9418  chlejb1t 9430  chnlet 9432  pjoml2t 9549  pjoml3t 9550  lecmt 9555  stcltr1 10196  mdbrt 10216  dmdmdt 10222  dmdit 10224  dmdbr3 10227  dmdbr4 10228  mdsl1 10243  mdslmd1lem3 10249  mdslmd1lem4 10250  csmdsym 10256  hatomict 10282  chrelat2t 10292  atordt 10310  atcvat4 10319  fiv 10470  inposetlem 10475  inposet 10477  iseuctopg 10488  mapdiscn 10497  fillsb 10546  neifil 10553  fgsb 10555  efilcp 10556  fgsb2 10560  efilcp2 10561  limfillem1OLD 10578  isalg 10624  algi 10631

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