Theorem sseq1 3292

Description: Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)

Assertion

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

Proof of Theorem sseq1

Step	Hyp	Ref	Expression
1		eqss 3287	. 2 ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))
2		sstr2 3279	. . . 4 ⊢ (B ⊆ A → (A ⊆ C → B ⊆ C))
3	2	adantl 452	. . 3 ⊢ ((A ⊆ B ∧ B ⊆ A) → (A ⊆ C → B ⊆ C))
4		sstr2 3279	. . . 4 ⊢ (A ⊆ B → (B ⊆ C → A ⊆ C))
5	4	adantr 451	. . 3 ⊢ ((A ⊆ B ∧ B ⊆ A) → (B ⊆ C → A ⊆ C))
6	3, 5	impbid 183	. 2 ⊢ ((A ⊆ B ∧ B ⊆ A) → (A ⊆ C ↔ B ⊆ C))
7	1, 6	sylbi 187	1 ⊢ (A = B → (A ⊆ C ↔ B ⊆ C))

Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358   = wceq 1642   ⊆ wss 3257

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-ss 3259

This theorem is referenced by:  sseq12  3294  sseq1i  3295  sseq1d  3298  nssne2  3328  psseq1  3356  uneqdifeq  3638  sbss  3659  pwjust  3723  elpw  3728  elpwg  3729  pwpw0  3855  sssn  3864  ssunsn2  3865  pwsnALT  3882  unimax  3925  pwadjoin  4119  eqpw1  4162  opkelssetkg  4268  sspw1  4335  sspw12  4336  ssfin  4470  tfinnn  4534  brssetg  4757  iss  5000  fununi  5160  funcnvuni  5161  ffoss  5314  clos1eq1  5874  frd  5922  mapsspm  6021  mapsspw  6022  mapsn  6026  enprmaplem6  6081  ovcelem1  6171  ceex  6174  nclec  6195  lec0cg  6198  ltcpw1pwg  6202  sbthlem2  6204  nc0le1  6216  dflec3  6221  lenc  6223  ce2le  6233  tlenc1c  6240  nchoicelem10  6298  nchoicelem13  6301