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  3831  ssprr  3834  sstpr  3835  unimax  3922  trss  4191  elssabg  4233  bnd2  4258  exmidexmid  4281  exmidsssn  4287  exmidsssnc  4288  exmid1stab  4293  mss  4313  exss  4314  frforeq2  4437  ordtri2orexmid  4616  ontr2exmid  4618  onsucsssucexmid  4620  reg2exmidlema  4627  sucprcreg  4642  ordtri2or2exmid  4664  ontri2orexmidim  4665  onintexmid  4666  tfis  4676  tfisi  4680  elomssom  4698  nnregexmid  4714  releq  4803  xpsspw  4833  iss  5054  relcnvtr  5251  iotass  5299  fununi  5392  funcnvuni  5393  funimaexglem  5407  ffoss  5609  ssimaex  5700  tfrlem1  6465  el2oss1o  6602  nnsucsssuc  6651  qsss  6754  phpm  7040  ssfiexmid  7051  findcard2d  7066  findcard2sd  7067  diffifi  7069  isinfinf  7072  fiintim  7109  fisseneq  7112  fidcenumlemrk  7137  fidcenumlemr  7138  sbthlem2  7141  isbth  7150  ctssdclemr  7295  onntri45  7442  tapeq1  7454  elinp  7677  sup3exmid  9120  zfz1isolem1  11080  zfz1iso  11081  fimaxre2  11759  sumeq1  11887  fsum2d  11967  fsumabs  11997  fsumiun  12009  prodeq1f  12084  fprod2d  12155  exmidunben  13018  ctiunct  13032  ssomct  13037  restsspw  13303  lspval  14375  uniopn  14696  fiinopn  14699  fiinbas  14744  baspartn  14745  eltg2  14748  eltg3  14752  topbas  14762  clsval  14806  neival  14838  neiint  14840  neipsm  14849  opnneissb  14850  opnssneib  14851  innei  14858  restbasg  14863  cnpdis  14937  txbas  14953  eltx  14954  neitx  14963  txlm  14974  blssexps  15124  blssex  15125  neibl  15186  metrest  15201  xmettx  15205  tgioo  15249  tgqioo  15250  limcimolemlt  15359  recnprss  15382  dvmptfsum  15420  lpvtx  15900  bj-om  16409  bj-2inf  16410  bj-nntrans  16423  bj-omtrans  16428  subctctexmid  16479  domomsubct  16480  pw1nct  16482