Theorem sseq1 3251

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 3243	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3235	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3235	. . . 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 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  sseq12  3253  sseq1i  3254  sseq1d  3257  nssne2  3287  sbss  3604  pwjust  3657  elpw  3662  elpwg  3664  sssnr  3841  ssprr  3844  sstpr  3845  unimax  3932  trss  4201  elssabg  4243  bnd2  4269  exmidexmid  4292  exmidsssn  4298  exmidsssnc  4299  exmid1stab  4304  mss  4324  exss  4325  frforeq2  4448  ordtri2orexmid  4627  ontr2exmid  4629  onsucsssucexmid  4631  reg2exmidlema  4638  sucprcreg  4653  ordtri2or2exmid  4675  ontri2orexmidim  4676  onintexmid  4677  tfis  4687  tfisi  4691  elomssom  4709  nnregexmid  4725  releq  4814  xpsspw  4844  iss  5065  relcnvtr  5263  iotass  5311  fununi  5405  funcnvuni  5406  funimaexglem  5420  ffoss  5625  ssimaex  5716  tfrlem1  6517  el2oss1o  6654  nnsucsssuc  6703  qsss  6806  phpm  7095  ssfiexmid  7106  ssfiexmidt  7108  findcard2d  7123  findcard2sd  7124  diffifi  7126  isinfinf  7129  fiintim  7166  fisseneq  7170  fidcenumlemrk  7196  fidcenumlemr  7197  sbthlem2  7200  isbth  7209  ctssdclemr  7354  onntri45  7502  tapeq1  7514  elinp  7737  sup3exmid  9180  zfz1isolem1  11148  zfz1iso  11149  fimaxre2  11848  sumeq1  11976  fsum2d  12057  fsumabs  12087  fsumiun  12099  prodeq1f  12174  fprod2d  12245  exmidunben  13108  ctiunct  13122  ssomct  13127  restsspw  13393  lspval  14466  uniopn  14792  fiinopn  14795  fiinbas  14840  baspartn  14841  eltg2  14844  eltg3  14848  topbas  14858  clsval  14902  neival  14934  neiint  14936  neipsm  14945  opnneissb  14946  opnssneib  14947  innei  14954  restbasg  14959  cnpdis  15033  txbas  15049  eltx  15050  neitx  15059  txlm  15070  blssexps  15220  blssex  15221  neibl  15282  metrest  15297  xmettx  15301  tgioo  15345  tgqioo  15346  limcimolemlt  15455  recnprss  15478  dvmptfsum  15516  lpvtx  16000  issubgr2  16179  subgrprop2  16181  egrsubgr  16184  0uhgrsubgr  16186  bj-om  16633  bj-2inf  16634  bj-nntrans  16647  bj-omtrans  16652  subctctexmid  16702  domomsubct  16703  pw1nct  16705