Theorem sseq1 3271

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 3263	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3255	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3255	. . . 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 1402   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  sseq12  3273  sseq1i  3274  sseq1d  3277  nssne2  3307  vvin  3569  sbss  3635  pwjust  3689  elpw  3694  elpwg  3696  sssnr  3876  ssprr  3879  sstpr  3880  unimax  3967  trss  4236  elssabg  4282  bnd2  4308  exmidexmid  4331  exmidsssn  4337  exmidsssnc  4338  exmid1stab  4343  mss  4364  exss  4365  frforeq2  4488  ordtri2orexmid  4668  ontr2exmid  4670  onsucsssucexmid  4672  reg2exmidlema  4679  sucprcreg  4694  ordtri2or2exmid  4716  ontri2orexmidim  4717  onintexmid  4718  tfis  4728  tfisi  4732  elomssom  4750  nnregexmid  4766  releq  4855  xpsspw  4885  iss  5107  relcnvtr  5305  iotass  5353  fununi  5447  funcnvuni  5448  funimaexglem  5462  ffoss  5670  ssimaex  5761  tfrlem1  6573  el2oss1o  6710  nnsucsssuc  6759  qsss  6862  phpm  7161  ssfiexmid  7172  ssfiexmidt  7174  findcard2d  7189  findcard2sd  7190  diffifi  7192  isinfinf  7195  fiintim  7232  fisseneq  7236  fidcenumlemrk  7265  fidcenumlemr  7266  sbthlem2  7269  isbth  7278  ctssdclemr  7446  onntri45  7594  papeq1  7603  tapeq1  7612  elinp  7835  sup3exmid  9281  zfz1isolem1  11275  zfz1iso  11276  fimaxre2  11976  sumeq1  12104  fsum2d  12185  fsumabs  12215  fsumiun  12227  prodeq1f  12302  fprod2d  12373  exmidunben  13300  ctiunct  13314  ssomct  13319  restsspw  13586  lspval  14710  aspval  14998  uniopn  15085  fiinopn  15088  fiinbas  15133  baspartn  15134  eltg2  15137  eltg3  15141  topbas  15151  clsval  15195  neival  15227  neiint  15229  neipsm  15238  opnneissb  15239  opnssneib  15240  innei  15247  restbasg  15252  cnpdis  15326  txbas  15342  eltx  15343  neitx  15352  txlm  15363  blssexps  15513  blssex  15514  neibl  15575  metrest  15590  xmettx  15594  tgioo  15638  tgqioo  15639  limcimolemlt  15748  recnprss  15771  dvmptfsum  15809  lpvtx  16303  issubgr2  16482  subgrprop2  16484  egrsubgr  16487  0uhgrsubgr  16489  bj-om  16946  bj-2inf  16947  bj-nntrans  16960  bj-omtrans  16965  subctctexmid  17013  domomsubct  17014  pw1nct  17016