Theorem sseq1 3206

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 3198	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3190	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3190	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 276	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 129	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 121	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1364   ⊆ wss 3157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  sseq12  3208  sseq1i  3209  sseq1d  3212  nssne2  3242  sbss  3558  pwjust  3606  elpw  3611  elpwg  3613  sssnr  3783  ssprr  3786  sstpr  3787  unimax  3873  trss  4140  elssabg  4181  bnd2  4206  exmidexmid  4229  exmidsssn  4235  exmidsssnc  4236  exmid1stab  4241  mss  4259  exss  4260  frforeq2  4380  ordtri2orexmid  4559  ontr2exmid  4561  onsucsssucexmid  4563  reg2exmidlema  4570  sucprcreg  4585  ordtri2or2exmid  4607  ontri2orexmidim  4608  onintexmid  4609  tfis  4619  tfisi  4623  elomssom  4641  nnregexmid  4657  releq  4745  xpsspw  4775  iss  4992  relcnvtr  5189  iotass  5236  fununi  5326  funcnvuni  5327  funimaexglem  5341  ffoss  5536  ssimaex  5622  tfrlem1  6366  el2oss1o  6501  nnsucsssuc  6550  qsss  6653  phpm  6926  ssfiexmid  6937  findcard2d  6952  findcard2sd  6953  diffifi  6955  isinfinf  6958  fiintim  6992  fisseneq  6995  fidcenumlemrk  7020  fidcenumlemr  7021  sbthlem2  7024  isbth  7033  ctssdclemr  7178  onntri45  7308  tapeq1  7319  elinp  7541  sup3exmid  8984  zfz1isolem1  10932  zfz1iso  10933  fimaxre2  11392  sumeq1  11520  fsum2d  11600  fsumabs  11630  fsumiun  11642  prodeq1f  11717  fprod2d  11788  exmidunben  12643  ctiunct  12657  ssomct  12662  restsspw  12920  lspval  13946  uniopn  14237  fiinopn  14240  fiinbas  14285  baspartn  14286  eltg2  14289  eltg3  14293  topbas  14303  clsval  14347  neival  14379  neiint  14381  neipsm  14390  opnneissb  14391  opnssneib  14392  innei  14399  restbasg  14404  cnpdis  14478  txbas  14494  eltx  14495  neitx  14504  txlm  14515  blssexps  14665  blssex  14666  neibl  14727  metrest  14742  xmettx  14746  tgioo  14790  tgqioo  14791  limcimolemlt  14900  recnprss  14923  dvmptfsum  14961  bj-om  15583  bj-2inf  15584  bj-nntrans  15597  bj-omtrans  15602  subctctexmid  15645  pw1nct  15647