Theorem sseq1 2966

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

Assertion

Ref	Expression
sseq1	⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Proof of Theorem sseq1

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

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

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 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931

This theorem is referenced by:  sseq12  2968  sseq1i  2969  sseq1d  2972  nssne2  3002  psseq1  3031  sspsstr  3050  sbss  3329  pwjust  3360  elpw  3365  elpwg  3367  sssnr  3524  ssprr  3527  sstpr  3528  unimax  3614  trss  3863  elssabg  3902  bnd2  3926  mss  3962  exss  3963  frforeq2  4082  ordtri2orexmid  4248  ontr2exmid  4250  onsucsssucexmid  4252  reg2exmidlema  4259  sucprcreg  4273  ordtri2or2exmid  4296  onintexmid  4297  tfis  4306  tfisi  4310  elnn  4328  nnregexmid  4342  releq  4422  xpsspw  4450  iss  4654  relcnvtr  4840  iotass  4884  fununi  4967  funcnvuni  4968  funimaexglem  4982  ffoss  5158  ssimaex  5234  tfrlem1  5923  nnsucsssuc  6071  qsss  6165  phpm  6327  ssfiexmid  6336  findcard2d  6348  findcard2sd  6349  diffifi  6351  elinp  6572  sumeq1  9874  bj-om  10061  bj-2inf  10062  bj-nntrans  10076  bj-omtrans  10081