Theorem sseq1 3120

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 3112	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3104	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 275	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3104	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
5	4	adantr 274	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐵 ⊆ 𝐶 → 𝐴 ⊆ 𝐶))
6	3, 5	impbid 128	. 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
7	1, 6	sylbi 120	1 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331   ⊆ wss 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  sseq12  3122  sseq1i  3123  sseq1d  3126  nssne2  3156  sbss  3471  pwjust  3511  elpw  3516  elpwg  3518  sssnr  3680  ssprr  3683  sstpr  3684  unimax  3770  trss  4035  elssabg  4073  bnd2  4097  exmidexmid  4120  exmidsssn  4125  exmidsssnc  4126  mss  4148  exss  4149  frforeq2  4267  ordtri2orexmid  4438  ontr2exmid  4440  onsucsssucexmid  4442  reg2exmidlema  4449  sucprcreg  4464  ordtri2or2exmid  4486  onintexmid  4487  tfis  4497  tfisi  4501  elnn  4519  nnregexmid  4534  releq  4621  xpsspw  4651  iss  4865  relcnvtr  5058  iotass  5105  fununi  5191  funcnvuni  5192  funimaexglem  5206  ffoss  5399  ssimaex  5482  tfrlem1  6205  nnsucsssuc  6388  qsss  6488  phpm  6759  ssfiexmid  6770  findcard2d  6785  findcard2sd  6786  diffifi  6788  isinfinf  6791  fiintim  6817  fisseneq  6820  fidcenumlemrk  6842  fidcenumlemr  6843  sbthlem2  6846  isbth  6855  ctssdclemr  6997  elinp  7282  sup3exmid  8715  zfz1isolem1  10583  zfz1iso  10584  fimaxre2  10998  sumeq1  11124  fsum2d  11204  fsumabs  11234  fsumiun  11246  prodeq1f  11321  exmidunben  11939  ctiunct  11953  restsspw  12130  uniopn  12168  fiinopn  12171  fiinbas  12216  baspartn  12217  eltg2  12222  eltg3  12226  topbas  12236  clsval  12280  neival  12312  neiint  12314  neipsm  12323  opnneissb  12324  opnssneib  12325  innei  12332  restbasg  12337  cnpdis  12411  txbas  12427  eltx  12428  neitx  12437  txlm  12448  blssexps  12598  blssex  12599  neibl  12660  metrest  12675  xmettx  12679  tgioo  12715  tgqioo  12716  limcimolemlt  12802  recnprss  12825  bj-om  13135  bj-2inf  13136  bj-nntrans  13149  bj-omtrans  13154  el2oss1o  13188  exmid1stab  13195  subctctexmid  13196