Theorem sseq1 3207

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 3199	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3191	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3191	. . . 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  3209  sseq1i  3210  sseq1d  3213  nssne2  3243  sbss  3559  pwjust  3607  elpw  3612  elpwg  3614  sssnr  3784  ssprr  3787  sstpr  3788  unimax  3874  trss  4141  elssabg  4182  bnd2  4207  exmidexmid  4230  exmidsssn  4236  exmidsssnc  4237  exmid1stab  4242  mss  4260  exss  4261  frforeq2  4381  ordtri2orexmid  4560  ontr2exmid  4562  onsucsssucexmid  4564  reg2exmidlema  4571  sucprcreg  4586  ordtri2or2exmid  4608  ontri2orexmidim  4609  onintexmid  4610  tfis  4620  tfisi  4624  elomssom  4642  nnregexmid  4658  releq  4746  xpsspw  4776  iss  4993  relcnvtr  5190  iotass  5237  fununi  5327  funcnvuni  5328  funimaexglem  5342  ffoss  5539  ssimaex  5625  tfrlem1  6375  el2oss1o  6510  nnsucsssuc  6559  qsss  6662  phpm  6935  ssfiexmid  6946  findcard2d  6961  findcard2sd  6962  diffifi  6964  isinfinf  6967  fiintim  7001  fisseneq  7004  fidcenumlemrk  7029  fidcenumlemr  7030  sbthlem2  7033  isbth  7042  ctssdclemr  7187  onntri45  7326  tapeq1  7337  elinp  7560  sup3exmid  9003  zfz1isolem1  10951  zfz1iso  10952  fimaxre2  11411  sumeq1  11539  fsum2d  11619  fsumabs  11649  fsumiun  11661  prodeq1f  11736  fprod2d  11807  exmidunben  12670  ctiunct  12684  ssomct  12689  restsspw  12953  lspval  14024  uniopn  14323  fiinopn  14326  fiinbas  14371  baspartn  14372  eltg2  14375  eltg3  14379  topbas  14389  clsval  14433  neival  14465  neiint  14467  neipsm  14476  opnneissb  14477  opnssneib  14478  innei  14485  restbasg  14490  cnpdis  14564  txbas  14580  eltx  14581  neitx  14590  txlm  14601  blssexps  14751  blssex  14752  neibl  14813  metrest  14828  xmettx  14832  tgioo  14876  tgqioo  14877  limcimolemlt  14986  recnprss  15009  dvmptfsum  15047  bj-om  15669  bj-2inf  15670  bj-nntrans  15683  bj-omtrans  15688  subctctexmid  15733  domomsubct  15734  pw1nct  15736