Theorem sseq1 3218

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 3210	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3202	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3202	. . . 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 1373   ⊆ wss 3168

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3174  df-ss 3181

This theorem is referenced by:  sseq12  3220  sseq1i  3221  sseq1d  3224  nssne2  3254  sbss  3570  pwjust  3619  elpw  3624  elpwg  3626  sssnr  3797  ssprr  3800  sstpr  3801  unimax  3887  trss  4156  elssabg  4197  bnd2  4222  exmidexmid  4245  exmidsssn  4251  exmidsssnc  4252  exmid1stab  4257  mss  4275  exss  4276  frforeq2  4397  ordtri2orexmid  4576  ontr2exmid  4578  onsucsssucexmid  4580  reg2exmidlema  4587  sucprcreg  4602  ordtri2or2exmid  4624  ontri2orexmidim  4625  onintexmid  4626  tfis  4636  tfisi  4640  elomssom  4658  nnregexmid  4674  releq  4762  xpsspw  4792  iss  5011  relcnvtr  5208  iotass  5255  fununi  5348  funcnvuni  5349  funimaexglem  5363  ffoss  5563  ssimaex  5650  tfrlem1  6404  el2oss1o  6539  nnsucsssuc  6588  qsss  6691  phpm  6974  ssfiexmid  6985  findcard2d  7000  findcard2sd  7001  diffifi  7003  isinfinf  7006  fiintim  7040  fisseneq  7043  fidcenumlemrk  7068  fidcenumlemr  7069  sbthlem2  7072  isbth  7081  ctssdclemr  7226  onntri45  7366  tapeq1  7377  elinp  7600  sup3exmid  9043  zfz1isolem1  10998  zfz1iso  10999  fimaxre2  11588  sumeq1  11716  fsum2d  11796  fsumabs  11826  fsumiun  11838  prodeq1f  11913  fprod2d  11984  exmidunben  12847  ctiunct  12861  ssomct  12866  restsspw  13131  lspval  14202  uniopn  14523  fiinopn  14526  fiinbas  14571  baspartn  14572  eltg2  14575  eltg3  14579  topbas  14589  clsval  14633  neival  14665  neiint  14667  neipsm  14676  opnneissb  14677  opnssneib  14678  innei  14685  restbasg  14690  cnpdis  14764  txbas  14780  eltx  14781  neitx  14790  txlm  14801  blssexps  14951  blssex  14952  neibl  15013  metrest  15028  xmettx  15032  tgioo  15076  tgqioo  15077  limcimolemlt  15186  recnprss  15209  dvmptfsum  15247  lpvtx  15725  bj-om  15987  bj-2inf  15988  bj-nntrans  16001  bj-omtrans  16006  subctctexmid  16052  domomsubct  16053  pw1nct  16055