Theorem sseq1i 4037

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

Syntax hints:   ↔ wb 206   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  eqsstri  4043  eqsstrid  4057  ssab  4087  rabss  4095  uniiunlem  4110  prssg  4844  sstp  4861  tpss  4862  iunssf  5067  iunss  5068  pwtr  5472  iunopeqop  5540  pwssun  5590  cores2  6290  resssxp  6301  sspred  6341  dffun2OLDOLD  6585  sbcfg  6745  idref  7180  ovmptss  8134  fnsuppres  8232  frrlem7  8333  ordgt0ge1  8549  omopthlem1  8715  naddasslem1  8750  naddasslem2  8751  dmttrcl  9790  trcl  9797  rankbnd  9937  rankbnd2  9938  rankc1  9939  dfac12a  10218  fin23lem34  10415  axdc2lem  10517  alephval2  10641  indpi  10976  fsuppmapnn0fiublem  14041  prodeq1i  15964  0ram  17067  mreacs  17716  lsslinds  21874  2ndcctbss  23484  xkoinjcn  23716  restmetu  24604  xrlimcnp  27029  mptelee  28928  ausgrusgrb  29200  nbuhgr2vtx1edgblem  29386  nbgrsym  29398  isuvtx  29430  2wlkdlem6  29964  frcond1  30298  n4cyclfrgr  30323  shlesb1i  31418  mdsldmd1i  32363  csmdsymi  32366  lfuhgr  35085  2cycl2d  35107  dfon2lem3  35749  dfon2lem7  35753  cbvprodvw2  36213  filnetlem4  36347  ptrecube  37580  poimirlem30  37610  idinxpssinxp2  38274  cossssid2  38424  symrefref2  38519  redundeq1  38585  funALTVfun  38654  disjxrn  38702  omabs2  43294  undmrnresiss  43566  clcnvlem  43585  cnvtrrel  43632  brtrclfv2  43689  dfhe3  43737  dffrege76  43901  mnurndlem1  44250  ssabf  45002  rabssf  45021  imassmpt  45172  clnbgrsym  47710  sclnbgrelself  47720  setrec2  48787