Theorem sseq1 3247

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 3239	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
2		sstr2 3231	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
3	2	adantl 277	. . 3 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴) → (𝐴 ⊆ 𝐶 → 𝐵 ⊆ 𝐶))
4		sstr2 3231	. . . 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 1395   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  sseq12  3249  sseq1i  3250  sseq1d  3253  nssne2  3283  sbss  3599  pwjust  3650  elpw  3655  elpwg  3657  sssnr  3831  ssprr  3834  sstpr  3835  unimax  3922  trss  4191  elssabg  4232  bnd2  4257  exmidexmid  4280  exmidsssn  4286  exmidsssnc  4287  exmid1stab  4292  mss  4312  exss  4313  frforeq2  4436  ordtri2orexmid  4615  ontr2exmid  4617  onsucsssucexmid  4619  reg2exmidlema  4626  sucprcreg  4641  ordtri2or2exmid  4663  ontri2orexmidim  4664  onintexmid  4665  tfis  4675  tfisi  4679  elomssom  4697  nnregexmid  4713  releq  4801  xpsspw  4831  iss  5051  relcnvtr  5248  iotass  5296  fununi  5389  funcnvuni  5390  funimaexglem  5404  ffoss  5606  ssimaex  5697  tfrlem1  6460  el2oss1o  6597  nnsucsssuc  6646  qsss  6749  phpm  7035  ssfiexmid  7046  findcard2d  7061  findcard2sd  7062  diffifi  7064  isinfinf  7067  fiintim  7101  fisseneq  7104  fidcenumlemrk  7129  fidcenumlemr  7130  sbthlem2  7133  isbth  7142  ctssdclemr  7287  onntri45  7434  tapeq1  7446  elinp  7669  sup3exmid  9112  zfz1isolem1  11070  zfz1iso  11071  fimaxre2  11746  sumeq1  11874  fsum2d  11954  fsumabs  11984  fsumiun  11996  prodeq1f  12071  fprod2d  12142  exmidunben  13005  ctiunct  13019  ssomct  13024  restsspw  13290  lspval  14362  uniopn  14683  fiinopn  14686  fiinbas  14731  baspartn  14732  eltg2  14735  eltg3  14739  topbas  14749  clsval  14793  neival  14825  neiint  14827  neipsm  14836  opnneissb  14837  opnssneib  14838  innei  14845  restbasg  14850  cnpdis  14924  txbas  14940  eltx  14941  neitx  14950  txlm  14961  blssexps  15111  blssex  15112  neibl  15173  metrest  15188  xmettx  15192  tgioo  15236  tgqioo  15237  limcimolemlt  15346  recnprss  15369  dvmptfsum  15407  lpvtx  15887  bj-om  16324  bj-2inf  16325  bj-nntrans  16338  bj-omtrans  16343  subctctexmid  16395  domomsubct  16396  pw1nct  16398