Theorem sseq1i 3959

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 3956	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  eqsstrid  3969  eqsstri  3977  ssab  4011  rabss  4018  uniiunlem  4035  prssg  4780  sstp  4796  tpss  4797  iunssfOLD  5002  iunssOLD  5004  pwtr  5420  iunopeqop  5494  iunopeqopOLD  5495  pwssun  5543  imadifssran  6195  imadifssranOLD  6196  cores2  6254  resssxp  6265  sspred  6306  sbcfg  6699  idref  7141  ovmptss  8093  fnsuppres  8192  frrlem7  8294  ordgt0ge1  8485  omopthlem1  8652  naddasslem1  8688  naddasslem2  8689  dmttrcl  9706  trcl  9713  rankbnd  9866  rankbnd2  9867  rankc1  9868  setrec2  9958  dfac12a  10208  fin23lem34  10405  alephval2  10638  indpi  10973  fsuppmapnn0fiublem  14113  prodeq1i  16065  0ram  17178  mreacs  17812  lsslinds  22117  2ndcctbss  23754  xkoinjcn  23986  restmetu  24869  xrlimcnp  27278  mpteleeOLD  29455  lfuhgr  29708  ausgrusgrb  29728  nbuhgr2vtx1edgblem  29914  nbgrsym  29926  isuvtx  29958  2wlkdlem6  30502  frcond1  30849  n4cyclfrgr  30874  shlesb1i  31970  mdsldmd1i  32915  csmdsymi  32918  tpssg  33115  2cycl2d  35881  dfon2lem3  36517  dfon2lem7  36521  cbvprodvw2  37006  filnetlem4  37139  ptrecube  38506  poimirlem30  38536  idinxpssinxp2  39224  cossssid2  39458  symrefref2  39547  redundeq1  39613  funALTVfun  39683  disjxrn  39746  omabs2  44292  undmrnresiss  44563  clcnvlem  44582  cnvtrrel  44629  brtrclfv2  44686  dfhe3  44734  dffrege76  44898  mnurndlem1  45224  ssabf  46058  rabssf  46077  imassmpt  46217  clnbgrsym  48880  sclnbgrelself  48890