Theorem sseq1i 3963

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  eqsstrid  3973  eqsstri  3981  ssab  4015  rabss  4022  uniiunlem  4037  prssg  4771  sstp  4788  tpss  4789  iunssf  4993  iunss  4994  pwtr  5393  iunopeqop  5461  pwssun  5508  imadifssran  6098  cores2  6207  resssxp  6217  sspred  6257  sbcfg  6649  idref  7079  ovmptss  8023  fnsuppres  8121  frrlem7  8222  ordgt0ge1  8408  omopthlem1  8574  naddasslem1  8609  naddasslem2  8610  dmttrcl  9611  trcl  9618  rankbnd  9758  rankbnd2  9759  rankc1  9760  dfac12a  10037  fin23lem34  10234  axdc2lem  10336  alephval2  10460  indpi  10795  fsuppmapnn0fiublem  13894  prodeq1i  15820  0ram  16929  mreacs  17561  lsslinds  21766  2ndcctbss  23368  xkoinjcn  23600  restmetu  24483  xrlimcnp  26903  mptelee  28871  ausgrusgrb  29141  nbuhgr2vtx1edgblem  29327  nbgrsym  29339  isuvtx  29371  2wlkdlem6  29907  frcond1  30241  n4cyclfrgr  30266  shlesb1i  31361  mdsldmd1i  32306  csmdsymi  32309  tpssg  32512  lfuhgr  35150  2cycl2d  35171  dfon2lem3  35818  dfon2lem7  35822  cbvprodvw2  36280  filnetlem4  36414  ptrecube  37659  poimirlem30  37689  idinxpssinxp2  38351  cossssid2  38504  symrefref2  38599  redundeq1  38665  funALTVfun  38735  disjxrn  38783  omabs2  43364  undmrnresiss  43636  clcnvlem  43655  cnvtrrel  43702  brtrclfv2  43759  dfhe3  43807  dffrege76  43971  mnurndlem1  44313  ssabf  45136  rabssf  45155  imassmpt  45298  clnbgrsym  47868  sclnbgrelself  47878  setrec2  49726