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  6583  el2oss1o  6720  nnsucsssuc  6769  qsss  6872  phpm  7171  ssfiexmid  7182  ssfiexmidt  7184  findcard2d  7199  findcard2sd  7200  diffifi  7202  isinfinf  7205  fiintim  7242  fisseneq  7246  fidcenumlemrk  7276  fidcenumlemr  7277  sbthlem2  7280  isbth  7289  ctssdclemr  7458  onntri45  7606  papeq1  7615  tapeq1  7624  elinp  7847  sup3exmid  9295  zfz1isolem1  11314  zfz1iso  11315  fimaxre2  12016  sumeq1  12146  fsum2d  12227  fsumabs  12257  fsumiun  12269  prodeq1f  12344  fprod2d  12415  exmidunben  13375  ctiunct  13389  ssomct  13394  restsspw  13662  lspval  14836  aspval  15124  uniopn  15227  fiinopn  15230  fiinbas  15275  baspartn  15276  eltg2  15279  eltg3  15283  topbas  15293  clsval  15337  neival  15369  neiint  15371  neipsm  15380  opnneissb  15381  opnssneib  15382  innei  15389  restbasg  15394  cnpdis  15468  txbas  15484  eltx  15485  neitx  15494  txlm  15505  blssexps  15655  blssex  15656  neibl  15717  metrest  15732  xmettx  15736  tgioo  15780  tgqioo  15781  limcimolemlt  15890  recnprss  15913  dvmptfsum  15951  lpvtx  16525  issubgr2  16704  subgrprop2  16706  egrsubgr  16709  0uhgrsubgr  16711  bj-om  17168  bj-2inf  17169  bj-nntrans  17182  bj-omtrans  17187  subctctexmid  17235  domomsubct  17236  pw1nct  17238