Theorem sseq1 3247

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 3239	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3231	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3231	. . . 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 1395   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sseq12  3249  sseq1i  3250  sseq1d  3253  nssne2  3283  sbss  3599  pwjust  3650  elpw  3655  elpwg  3657  sssnr  3830  ssprr  3833  sstpr  3834  unimax  3921  trss  4190  elssabg  4231  bnd2  4256  exmidexmid  4279  exmidsssn  4285  exmidsssnc  4286  exmid1stab  4291  mss  4311  exss  4312  frforeq2  4433  ordtri2orexmid  4612  ontr2exmid  4614  onsucsssucexmid  4616  reg2exmidlema  4623  sucprcreg  4638  ordtri2or2exmid  4660  ontri2orexmidim  4661  onintexmid  4662  tfis  4672  tfisi  4676  elomssom  4694  nnregexmid  4710  releq  4798  xpsspw  4828  iss  5047  relcnvtr  5244  iotass  5292  fununi  5385  funcnvuni  5386  funimaexglem  5400  ffoss  5600  ssimaex  5688  tfrlem1  6444  el2oss1o  6579  nnsucsssuc  6628  qsss  6731  phpm  7015  ssfiexmid  7026  findcard2d  7041  findcard2sd  7042  diffifi  7044  isinfinf  7047  fiintim  7081  fisseneq  7084  fidcenumlemrk  7109  fidcenumlemr  7110  sbthlem2  7113  isbth  7122  ctssdclemr  7267  onntri45  7414  tapeq1  7426  elinp  7649  sup3exmid  9092  zfz1isolem1  11049  zfz1iso  11050  fimaxre2  11724  sumeq1  11852  fsum2d  11932  fsumabs  11962  fsumiun  11974  prodeq1f  12049  fprod2d  12120  exmidunben  12983  ctiunct  12997  ssomct  13002  restsspw  13268  lspval  14339  uniopn  14660  fiinopn  14663  fiinbas  14708  baspartn  14709  eltg2  14712  eltg3  14716  topbas  14726  clsval  14770  neival  14802  neiint  14804  neipsm  14813  opnneissb  14814  opnssneib  14815  innei  14822  restbasg  14827  cnpdis  14901  txbas  14917  eltx  14918  neitx  14927  txlm  14938  blssexps  15088  blssex  15089  neibl  15150  metrest  15165  xmettx  15169  tgioo  15213  tgqioo  15214  limcimolemlt  15323  recnprss  15346  dvmptfsum  15384  lpvtx  15864  bj-om  16230  bj-2inf  16231  bj-nntrans  16244  bj-omtrans  16249  subctctexmid  16297  domomsubct  16298  pw1nct  16300