Theorem sseq1 2943

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 ⊆ 𝐶 ↔ B ⊆ 𝐶))

Proof of Theorem sseq1

Step	Hyp	Ref	Expression
1		eqss 2937	. 2 ⊢ (A = B ↔ (A ⊆ B ∧ B ⊆ A))
2		sstr2 2929	. . . 4 ⊢ (B ⊆ A → (A ⊆ 𝐶 → B ⊆ 𝐶))
3	2	adantl 262	. . 3 ⊢ ((A ⊆ B ∧ B ⊆ A) → (A ⊆ 𝐶 → B ⊆ 𝐶))
4		sstr2 2929	. . . 4 ⊢ (A ⊆ B → (B ⊆ 𝐶 → A ⊆ 𝐶))
5	4	adantr 261	. . 3 ⊢ ((A ⊆ B ∧ B ⊆ A) → (B ⊆ 𝐶 → A ⊆ 𝐶))
6	3, 5	impbid 120	. 2 ⊢ ((A ⊆ B ∧ B ⊆ A) → (A ⊆ 𝐶 ↔ B ⊆ 𝐶))
7	1, 6	sylbi 114	1 ⊢ (A = B → (A ⊆ 𝐶 ↔ B ⊆ 𝐶))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98   = wceq 1228   ⊆ wss 2894

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004

This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-in 2901  df-ss 2908

This theorem is referenced by:  sseq12  2945  sseq1i  2946  sseq1d  2949  nssne2  2979  psseq1  3008  sspsstr  3027  sbss  3308  pwjust  3335  elpw  3340  elpwg  3342  sssnr  3498  ssprr  3501  sstpr  3502  unimax  3588  trss  3837  elssabg  3876  bnd2  3900  mss  3936  exss  3937  ordtri2orexmid  4195  onsucsssucexmid  4196  sucprcreg  4211  tfis  4233  tfisi  4237  elnn  4255  nnregexmid  4269  releq  4349  xpsspw  4377  iss  4581  relcnvtr  4767  iotass  4811  fununi  4893  funcnvuni  4894  funimaexglem  4908  ffoss  5083  ssimaex  5159  tfrlem1  5845  nnsucsssuc  5986  qsss  6076  elinp  6328  bj-om  7159  bj-2inf  7160  bj-nntrans  7173  bj-omtrans  7178