Theorem sseq1 3260

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 3252	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3244	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3244	. . . 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 1398   ⊆ wss 3210

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  sseq12  3262  sseq1i  3263  sseq1d  3266  nssne2  3296  sbss  3616  pwjust  3669  elpw  3674  elpwg  3676  sssnr  3856  ssprr  3859  sstpr  3860  unimax  3947  trss  4216  elssabg  4259  bnd2  4285  exmidexmid  4308  exmidsssn  4314  exmidsssnc  4315  exmid1stab  4320  mss  4341  exss  4342  frforeq2  4465  ordtri2orexmid  4644  ontr2exmid  4646  onsucsssucexmid  4648  reg2exmidlema  4655  sucprcreg  4670  ordtri2or2exmid  4692  ontri2orexmidim  4693  onintexmid  4694  tfis  4704  tfisi  4708  elomssom  4726  nnregexmid  4742  releq  4831  xpsspw  4861  iss  5083  relcnvtr  5281  iotass  5329  fununi  5423  funcnvuni  5424  funimaexglem  5438  ffoss  5646  ssimaex  5737  tfrlem1  6538  el2oss1o  6675  nnsucsssuc  6724  qsss  6827  phpm  7119  ssfiexmid  7130  ssfiexmidt  7132  findcard2d  7147  findcard2sd  7148  diffifi  7150  isinfinf  7153  fiintim  7190  fisseneq  7194  fidcenumlemrk  7223  fidcenumlemr  7224  sbthlem2  7227  isbth  7236  ctssdclemr  7402  onntri45  7550  tapeq1  7565  elinp  7788  sup3exmid  9230  zfz1isolem1  11208  zfz1iso  11209  fimaxre2  11908  sumeq1  12036  fsum2d  12117  fsumabs  12147  fsumiun  12159  prodeq1f  12234  fprod2d  12305  exmidunben  13169  ctiunct  13183  ssomct  13188  restsspw  13454  lspval  14530  uniopn  14858  fiinopn  14861  fiinbas  14906  baspartn  14907  eltg2  14910  eltg3  14914  topbas  14924  clsval  14968  neival  15000  neiint  15002  neipsm  15011  opnneissb  15012  opnssneib  15013  innei  15020  restbasg  15025  cnpdis  15099  txbas  15115  eltx  15116  neitx  15125  txlm  15136  blssexps  15286  blssex  15287  neibl  15348  metrest  15363  xmettx  15367  tgioo  15411  tgqioo  15412  limcimolemlt  15521  recnprss  15544  dvmptfsum  15582  lpvtx  16066  issubgr2  16245  subgrprop2  16247  egrsubgr  16250  0uhgrsubgr  16252  bj-om  16699  bj-2inf  16700  bj-nntrans  16713  bj-omtrans  16718  subctctexmid  16766  domomsubct  16767  pw1nct  16769