Theorem sseq1i 3975

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

Syntax hints:   ↔ wb 205   = wceq 1541   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-in 3920  df-ss 3930

This theorem is referenced by:  eqsstri  3981  eqsstrid  3995  ssab  4023  rabss  4034  uniiunlem  4049  prssg  4784  sstp  4799  tpss  4800  iunssf  5009  iunss  5010  pwtr  5414  iunopeqop  5483  pwssun  5533  cores2  6216  resssxp  6227  sspred  6267  dffun2OLDOLD  6513  sbcfg  6671  idref  7097  ovmptss  8030  fnsuppres  8127  frrlem7  8228  ordgt0ge1  8444  omopthlem1  8610  naddasslem1  8645  naddasslem2  8646  dmttrcl  9666  trcl  9673  rankbnd  9813  rankbnd2  9814  rankc1  9815  dfac12a  10093  fin23lem34  10291  axdc2lem  10393  alephval2  10517  indpi  10852  fsuppmapnn0fiublem  13905  0ram  16903  mreacs  17552  lsslinds  21274  2ndcctbss  22843  xkoinjcn  23075  restmetu  23963  xrlimcnp  26355  mptelee  27907  ausgrusgrb  28179  nbuhgr2vtx1edgblem  28362  nbgrsym  28374  isuvtx  28406  2wlkdlem6  28939  frcond1  29273  n4cyclfrgr  29298  shlesb1i  30391  mdsldmd1i  31336  csmdsymi  31339  lfuhgr  33798  2cycl2d  33820  dfon2lem3  34446  dfon2lem7  34450  filnetlem4  34929  ptrecube  36151  poimirlem30  36181  idinxpssinxp2  36852  cossssid2  37003  symrefref2  37098  redundeq1  37164  funALTVfun  37233  disjxrn  37281  omabs2  41725  undmrnresiss  41998  clcnvlem  42017  cnvtrrel  42064  brtrclfv2  42121  dfhe3  42169  dffrege76  42333  mnurndlem1  42683  ssabf  43432  rabssf  43451  imassmpt  43612  setrec2  47260