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  4240  elssabg  4286  bnd2  4312  exmidexmid  4335  exmidsssn  4341  exmidsssnc  4342  exmid1stab  4347  mss  4368  exss  4369  frforeq2  4492  ordtri2orexmid  4672  ontr2exmid  4674  onsucsssucexmid  4676  reg2exmidlema  4683  sucprcreg  4698  ordtri2or2exmid  4720  ontri2orexmidim  4721  onintexmid  4722  tfis  4732  tfisi  4736  elomssom  4754  nnregexmid  4770  releq  4859  xpsspw  4889  iss  5112  relcnvtr  5310  iotass  5358  fununi  5452  funcnvuni  5453  funimaexglem  5467  ffoss  5675  ssimaex  5767  tfrlem1  6584  el2oss1o  6721  nnsucsssuc  6770  qsss  6873  phpm  7173  ssfiexmid  7184  ssfiexmidt  7186  findcard2d  7201  findcard2sd  7202  diffifi  7204  isinfinf  7207  fiintim  7244  fisseneq  7248  fidcenumlemrk  7278  fidcenumlemr  7279  sbthlem2  7282  isbth  7291  isfsuppfid  7297  ctssdclemr  7458  onntri45  7606  papeq1  7615  tapeq1  7624  elinp  7847  sup3exmid  9295  zfz1isolem1  11313  zfz1iso  11314  fimaxre2  12015  sumeq1  12145  fsum2d  12226  fsumabs  12256  fsumiun  12268  prodeq1f  12343  fprod2d  12414  exmidunben  13374  ctiunct  13388  ssomct  13393  restsspw  13661  lspval  14835  aspval  15123  psrbagmax  15183  uniopn  15244  fiinopn  15247  fiinbas  15292  baspartn  15293  eltg2  15296  eltg3  15300  topbas  15310  clsval  15354  neival  15386  neiint  15388  neipsm  15397  opnneissb  15398  opnssneib  15399  innei  15406  restbasg  15411  cnpdis  15485  txbas  15501  eltx  15502  neitx  15511  txlm  15522  blssexps  15672  blssex  15673  neibl  15734  metrest  15749  xmettx  15753  tgioo  15797  tgqioo  15798  limcimolemlt  15907  recnprss  15930  dvmptfsum  15968  lpvtx  16542  issubgr2  16721  subgrprop2  16723  egrsubgr  16726  0uhgrsubgr  16728  bj-om  17185  bj-2inf  17186  bj-nntrans  17199  bj-omtrans  17204  subctctexmid  17252  domomsubct  17253  pw1nct  17255