Theorem sseq2 3294

Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)

Assertion

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

Proof of Theorem sseq2

Step	Hyp	Ref	Expression
1		sstr2 3280	. . . 4 ⊢ (C ⊆ A → (A ⊆ B → C ⊆ B))
2	1	com12 27	. . 3 ⊢ (A ⊆ B → (C ⊆ A → C ⊆ B))
3		sstr2 3280	. . . 4 ⊢ (C ⊆ B → (B ⊆ A → C ⊆ A))
4	3	com12 27	. . 3 ⊢ (B ⊆ A → (C ⊆ B → C ⊆ A))
5	2, 4	anim12i 549	. 2 ⊢ ((A ⊆ B ∧ B ⊆ A) → ((C ⊆ A → C ⊆ B) ∧ (C ⊆ B → C ⊆ A)))
6		eqss 3288	. 2 ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))
7		dfbi2 609	. 2 ⊢ ((C ⊆ A ↔ C ⊆ B) ↔ ((C ⊆ A → C ⊆ B) ∧ (C ⊆ B → C ⊆ A)))
8	5, 6, 7	3imtr4i 257	1 ⊢ (A = B → (C ⊆ A ↔ C ⊆ B))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-ss 3260

This theorem is referenced by:  sseq12  3295  sseq2i  3297  sseq2d  3300  syl5sseq  3320  nssne1  3328  psseq2  3358  sseq0  3583  un00  3587  disjpss  3602  pweq  3726  ssintab  3944  ssintub  3945  intmin  3947  p6eq  4239  opkelssetkg  4269  pw1equn  4332  pw1eqadj  4333  ssfin  4471  sfinltfin  4536  vfinspsslem1  4551  brssetg  4758  fununi  5161  funcnvuni  5162  feq3  5213  clos1induct  5881  frd  5923  nclec  6196  lecidg  6197  lecncvg  6200  ltcpw1pwg  6203  sbthlem2  6205  addlec  6209  nc0le1  6217  ce2le  6234  tlenc1c  6241