Theorem sseq1 1521

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

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

This theorem is referenced by:  sseq12 1523  sseq1i 1524  sseq1d 1527  psseq1 1559  elpw 1801  elpwg 1802  sssn 1852  prsspw 1858  nnullss 1880  exss 1881  pwpw0 1883  unisseq 1946  trss 2050  fri 2170  frc 2172  onssmin 2263  releq 2477  iss 2599  fununi 2705  funcnvuni 2706  fssxp 2761  ffoss 2820  isofrlem 2939  f1oweOLD 2944  tfrlem1 2949  oawordeu 3157  pw2en 3348  sbthlem2 3350  sbth 3359  php 3409  unbnn2 3436  fiint 3445  sucprcreg 3451  tz9.1 3490  setind 3492  rankr1 3518  rankr1id 3539  scott0 3542  bnd2 3549  aceq3lem 3555  ac6lem 3575  zornlem7 3609  oncard 3636  carduni 3664  cardaleph 3690  cflem 3700  cflim 3704  cflecard 3707  cfsuc 3709  infxpidmlem2 4934  infxpidmlem3 4935  infxpidmlem7 4939  infxpidmlem8 4940  infmap2lem1 4951  infmap2 4953  sh 5116  occlt 5189  omls 5251  shintclt 5295  chintclt 5297  spanvalt 5300  shlubt 5355  chnlen0 5369  chsscon3t 5417  chlejb1t 5429  chnlet 5431  h1datomt 5484  cmbr4 5510  pjoml3t 5517  osumlem8 5537  spansncvt 5543  pjcjt2 5580  pjss1co 5633  pjopytht 5662  stjt 5676  stcltr1 5707  mdi 5727  mdbr3 5729  mdbr4 5730  dmdbr 5731  atss 5744  atom1d 5750  chcv1t 5751  shatomic 5753  hatomistic 5755  chrelat2t 5761  atcvatlem 5770  atcvat4 5775  mdsymlem2 5777  mdsymlem3 5778  mdsymlem6 5781

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