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  7453  onntri45  7601  papeq1  7610  tapeq1  7619  elinp  7842  sup3exmid  9290  zfz1isolem1  11307  zfz1iso  11308  fimaxre2  12009  sumeq1  12139  fsum2d  12220  fsumabs  12250  fsumiun  12262  prodeq1f  12337  fprod2d  12408  exmidunben  13368  ctiunct  13382  ssomct  13387  restsspw  13654  lspval  14778  aspval  15066  uniopn  15154  fiinopn  15157  fiinbas  15202  baspartn  15203  eltg2  15206  eltg3  15210  topbas  15220  clsval  15264  neival  15296  neiint  15298  neipsm  15307  opnneissb  15308  opnssneib  15309  innei  15316  restbasg  15321  cnpdis  15395  txbas  15411  eltx  15412  neitx  15421  txlm  15432  blssexps  15582  blssex  15583  neibl  15644  metrest  15659  xmettx  15663  tgioo  15707  tgqioo  15708  limcimolemlt  15817  recnprss  15840  dvmptfsum  15878  lpvtx  16442  issubgr2  16621  subgrprop2  16623  egrsubgr  16626  0uhgrsubgr  16628  bj-om  17085  bj-2inf  17086  bj-nntrans  17099  bj-omtrans  17104  subctctexmid  17152  domomsubct  17153  pw1nct  17155