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  14345  fiinopn  14348  fiinbas  14393  baspartn  14394  eltg2  14397  eltg3  14401  topbas  14411  clsval  14455  neival  14487  neiint  14489  neipsm  14498  opnneissb  14499  opnssneib  14500  innei  14507  restbasg  14512  cnpdis  14586  txbas  14602  eltx  14603  neitx  14612  txlm  14623  blssexps  14773  blssex  14774  neibl  14835  metrest  14850  xmettx  14854  tgioo  14898  tgqioo  14899  limcimolemlt  15008  recnprss  15031  dvmptfsum  15069  bj-om  15691  bj-2inf  15692  bj-nntrans  15705  bj-omtrans  15710  subctctexmid  15755  domomsubct  15756  pw1nct  15758