Theorem sseq1 3180

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 3172	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3164	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3164	. . . 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 1353   ⊆ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  sseq12  3182  sseq1i  3183  sseq1d  3186  nssne2  3216  sbss  3533  pwjust  3578  elpw  3583  elpwg  3585  sssnr  3755  ssprr  3758  sstpr  3759  unimax  3845  trss  4112  elssabg  4150  bnd2  4175  exmidexmid  4198  exmidsssn  4204  exmidsssnc  4205  exmid1stab  4210  mss  4228  exss  4229  frforeq2  4347  ordtri2orexmid  4524  ontr2exmid  4526  onsucsssucexmid  4528  reg2exmidlema  4535  sucprcreg  4550  ordtri2or2exmid  4572  ontri2orexmidim  4573  onintexmid  4574  tfis  4584  tfisi  4588  elomssom  4606  nnregexmid  4622  releq  4710  xpsspw  4740  iss  4955  relcnvtr  5150  iotass  5197  fununi  5286  funcnvuni  5287  funimaexglem  5301  ffoss  5495  ssimaex  5580  tfrlem1  6312  el2oss1o  6447  nnsucsssuc  6496  qsss  6597  phpm  6868  ssfiexmid  6879  findcard2d  6894  findcard2sd  6895  diffifi  6897  isinfinf  6900  fiintim  6931  fisseneq  6934  fidcenumlemrk  6956  fidcenumlemr  6957  sbthlem2  6960  isbth  6969  ctssdclemr  7114  onntri45  7243  tapeq1  7254  elinp  7476  sup3exmid  8917  zfz1isolem1  10823  zfz1iso  10824  fimaxre2  11238  sumeq1  11366  fsum2d  11446  fsumabs  11476  fsumiun  11488  prodeq1f  11563  fprod2d  11634  exmidunben  12430  ctiunct  12444  ssomct  12449  restsspw  12704  lspval  13488  uniopn  13662  fiinopn  13665  fiinbas  13710  baspartn  13711  eltg2  13714  eltg3  13718  topbas  13728  clsval  13772  neival  13804  neiint  13806  neipsm  13815  opnneissb  13816  opnssneib  13817  innei  13824  restbasg  13829  cnpdis  13903  txbas  13919  eltx  13920  neitx  13929  txlm  13940  blssexps  14090  blssex  14091  neibl  14152  metrest  14167  xmettx  14171  tgioo  14207  tgqioo  14208  limcimolemlt  14294  recnprss  14317  bj-om  14850  bj-2inf  14851  bj-nntrans  14864  bj-omtrans  14869  subctctexmid  14912  pw1nct  14914