Theorem sseq2 1522

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 1510	. . . 4 ⊢ (C ⊆ A → (A ⊆ B → C ⊆ B))
2	1	com12 13	. . 3 ⊢ (A ⊆ B → (C ⊆ A → C ⊆ B))
3		sstr2 1510	. . . 4 ⊢ (C ⊆ B → (B ⊆ A → C ⊆ A))
4	3	com12 13	. . 3 ⊢ (B ⊆ A → (C ⊆ B → C ⊆ A))
5	2, 4	anim12i 268	. 2 ⊢ ((A ⊆ B ∧ B ⊆ A) → ((C ⊆ A → C ⊆ B) ∧ (C ⊆ B → C ⊆ A)))
6		eqss 1516	. 2 ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))
7		bi 396	. 2 ⊢ ((C ⊆ A ↔ C ⊆ B) ↔ ((C ⊆ A → C ⊆ B) ∧ (C ⊆ B → C ⊆ A)))
8	5, 6, 7	3imtr4 192	1 ⊢ (A = B → (C ⊆ A ↔ C ⊆ B))

Syntax hints:   → wi 2   ↔ wb 127   ∧ wa 196   = wceq 1091   ⊆ wss 1487

This theorem is referenced by:  sseq12 1523  sseq2i 1525  sseq2d 1528  eqimss 1548  psseq2 1560  ssexg 1702  un00 1728  disjpss 1738  pweq 1800  ssuni 1937  ssintub 1981  intmin 1982  iunpw 2040  treq 2047  ordunidif 2260  ordssun 2330  limomss 2378  findsg 2398  tfindsg 2402  fununi 2705  funcnvuni 2706  feq3 2750  oawordeu 3157  oawordexr 3158  ereq 3206  domeng 3285  undom 3342  sbthlem4 3352  sbthlem5 3353  mapdom2lem 3388  php3 3411  inf3lema 3460  tz9.1 3490  scottex 3541  aceq3 3556  ac7g 3570  cardlim 3657  isinfcard 3692  cflem 3700  cfval 3701  cflecard 3707  cfsuc 3709  infxpidmlem7 4939  infxpidmlem11 4943  omls 5251  ococint 5298  spanvalt 5300  hsupval2t 5301  spanclt 5305  chsupsn 5313  shlubt 5355  shsumval2 5361  chj00 5408  chsscon3t 5417  chlejb1t 5429  chnlet 5431  pjoml3t 5517  stcltr1 5707  mdbr 5726  dmdbr 5731  dmdi 5732  chrelat2t 5761  atcvat4 5775

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org