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 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ⊆ wss 3220

This proof depends on 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 proof 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 used by:  sseq12  3273  sseq1i  3274  sseq1d  3277  nssne2  3307  vvin  3569  sbss  3635  pwjust  3689  elpw  3694  elpwg  3696  sssnr  3878  ssprr  3881  sstpr  3882  unimax  3969  trss  4238  elssabg  4284  bnd2  4310  exmidexmid  4333  exmidsssn  4339  exmidsssnc  4340  exmid1stab  4345  mss  4366  exss  4367  frforeq2  4490  ordtri2orexmid  4670  ontr2exmid  4672  onsucsssucexmid  4674  reg2exmidlema  4681  sucprcreg  4696  ordtri2or2exmid  4718  ontri2orexmidim  4719  onintexmid  4720  tfis  4730  tfisi  4734  elomssom  4752  nnregexmid  4768  releq  4857  xpsspw  4887  iss  5109  relcnvtr  5307  iotass  5355  fununi  5449  funcnvuni  5450  funimaexglem  5464  ffoss  5672  ssimaex  5764  tfrlem1  6579  el2oss1o  6716  nnsucsssuc  6765  qsss  6868  phpm  7167  ssfiexmid  7178  ssfiexmidt  7180  findcard2d  7195  findcard2sd  7196  diffifi  7198  isinfinf  7201  fiintim  7238  fisseneq  7242  fidcenumlemrk  7271  fidcenumlemr  7272  sbthlem2  7275  isbth  7284  ctssdclemr  7452  onntri45  7600  papeq1  7609  tapeq1  7618  elinp  7841  sup3exmid  9288  zfz1isolem1  11294  zfz1iso  11295  fimaxre2  11995  sumeq1  12123  fsum2d  12204  fsumabs  12234  fsumiun  12246  prodeq1f  12321  fprod2d  12392  exmidunben  13319  ctiunct  13333  ssomct  13338  restsspw  13605  lspval  14729  aspval  15017  uniopn  15104  fiinopn  15107  fiinbas  15152  baspartn  15153  eltg2  15156  eltg3  15160  topbas  15170  clsval  15214  neival  15246  neiint  15248  neipsm  15257  opnneissb  15258  opnssneib  15259  innei  15266  restbasg  15271  cnpdis  15345  txbas  15361  eltx  15362  neitx  15371  txlm  15382  blssexps  15532  blssex  15533  neibl  15594  metrest  15609  xmettx  15613  tgioo  15657  tgqioo  15658  limcimolemlt  15767  recnprss  15790  dvmptfsum  15828  lpvtx  16332  issubgr2  16511  subgrprop2  16513  egrsubgr  16516  0uhgrsubgr  16518  bj-om  16975  bj-2inf  16976  bj-nntrans  16989  bj-omtrans  16994  subctctexmid  17042  domomsubct  17043  pw1nct  17045