Theorem sseq1 3151

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 3143	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3135	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 275	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3135	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 274	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 128	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 120	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1335   ⊆ wss 3102

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-11 1486  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-sb 1743  df-clab 2144  df-cleq 2150  df-clel 2153  df-in 3108  df-ss 3115

This theorem is referenced by:  sseq12  3153  sseq1i  3154  sseq1d  3157  nssne2  3187  sbss  3502  pwjust  3544  elpw  3549  elpwg  3551  sssnr  3716  ssprr  3719  sstpr  3720  unimax  3806  trss  4071  elssabg  4109  bnd2  4134  exmidexmid  4157  exmidsssn  4163  exmidsssnc  4164  mss  4186  exss  4187  frforeq2  4305  ordtri2orexmid  4481  ontr2exmid  4483  onsucsssucexmid  4485  reg2exmidlema  4492  sucprcreg  4507  ordtri2or2exmid  4529  ontri2orexmidim  4530  onintexmid  4531  tfis  4541  tfisi  4545  elomssom  4563  nnregexmid  4579  releq  4667  xpsspw  4697  iss  4911  relcnvtr  5104  iotass  5151  fununi  5237  funcnvuni  5238  funimaexglem  5252  ffoss  5445  ssimaex  5528  tfrlem1  6252  el2oss1o  6387  nnsucsssuc  6436  qsss  6536  phpm  6807  ssfiexmid  6818  findcard2d  6833  findcard2sd  6834  diffifi  6836  isinfinf  6839  fiintim  6870  fisseneq  6873  fidcenumlemrk  6895  fidcenumlemr  6896  sbthlem2  6899  isbth  6908  ctssdclemr  7050  onntri45  7170  elinp  7388  sup3exmid  8822  zfz1isolem1  10704  zfz1iso  10705  fimaxre2  11119  sumeq1  11245  fsum2d  11325  fsumabs  11355  fsumiun  11367  prodeq1f  11442  fprod2d  11513  exmidunben  12138  ctiunct  12152  restsspw  12332  uniopn  12370  fiinopn  12373  fiinbas  12418  baspartn  12419  eltg2  12424  eltg3  12428  topbas  12438  clsval  12482  neival  12514  neiint  12516  neipsm  12525  opnneissb  12526  opnssneib  12527  innei  12534  restbasg  12539  cnpdis  12613  txbas  12629  eltx  12630  neitx  12639  txlm  12650  blssexps  12800  blssex  12801  neibl  12862  metrest  12877  xmettx  12881  tgioo  12917  tgqioo  12918  limcimolemlt  13004  recnprss  13027  bj-om  13483  bj-2inf  13484  bj-nntrans  13497  bj-omtrans  13502  exmid1stab  13543  subctctexmid  13544  pw1nct  13546