Theorem sseq1i 3962

Description: An equality inference for the subclass relationship. (Contributed by NM, 18-Aug-1993.)

Hypothesis

Ref	Expression
sseq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
sseq1i	⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)

Proof of Theorem sseq1i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		sseq1 3959	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)

Syntax hints:   ↔ wb 206   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  eqsstrid  3972  eqsstri  3980  ssab  4015  rabss  4022  uniiunlem  4039  prssg  4775  sstp  4792  tpss  4793  iunssfOLD  4999  iunssOLD  5001  pwtr  5400  iunopeqop  5469  pwssun  5516  imadifssran  6109  cores2  6218  resssxp  6228  sspred  6268  sbcfg  6660  idref  7091  ovmptss  8035  fnsuppres  8133  frrlem7  8234  ordgt0ge1  8420  omopthlem1  8587  naddasslem1  8622  naddasslem2  8623  dmttrcl  9630  trcl  9637  rankbnd  9780  rankbnd2  9781  rankc1  9782  dfac12a  10059  fin23lem34  10256  alephval2  10483  indpi  10818  fsuppmapnn0fiublem  13913  prodeq1i  15839  0ram  16948  mreacs  17581  lsslinds  21786  2ndcctbss  23399  xkoinjcn  23631  restmetu  24514  xrlimcnp  26934  mpteleeOLD  28968  ausgrusgrb  29238  nbuhgr2vtx1edgblem  29424  nbgrsym  29436  isuvtx  29468  2wlkdlem6  30004  frcond1  30341  n4cyclfrgr  30366  shlesb1i  31461  mdsldmd1i  32406  csmdsymi  32409  tpssg  32612  lfuhgr  35312  2cycl2d  35333  dfon2lem3  35977  dfon2lem7  35981  cbvprodvw2  36441  filnetlem4  36575  ptrecube  37817  poimirlem30  37847  idinxpssinxp2  38513  cossssid2  38727  symrefref2  38816  redundeq1  38882  funALTVfun  38953  disjxrn  39001  omabs2  43570  undmrnresiss  43841  clcnvlem  43860  cnvtrrel  43907  brtrclfv2  43964  dfhe3  44012  dffrege76  44176  mnurndlem1  44518  ssabf  45340  rabssf  45359  imassmpt  45502  clnbgrsym  48080  sclnbgrelself  48090  setrec2  49936