Theorem sseq1i 4010

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

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

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 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965

This theorem is referenced by:  eqsstri  4016  eqsstrid  4030  ssab  4058  rabss  4069  uniiunlem  4084  prssg  4822  sstp  4837  tpss  4838  iunssf  5047  iunss  5048  pwtr  5452  iunopeqop  5521  pwssun  5571  cores2  6258  resssxp  6269  sspred  6309  dffun2OLDOLD  6555  sbcfg  6715  idref  7146  ovmptss  8081  fnsuppres  8178  frrlem7  8279  ordgt0ge1  8495  omopthlem1  8660  naddasslem1  8695  naddasslem2  8696  dmttrcl  9718  trcl  9725  rankbnd  9865  rankbnd2  9866  rankc1  9867  dfac12a  10145  fin23lem34  10343  axdc2lem  10445  alephval2  10569  indpi  10904  fsuppmapnn0fiublem  13959  0ram  16957  mreacs  17606  lsslinds  21605  2ndcctbss  23179  xkoinjcn  23411  restmetu  24299  xrlimcnp  26697  mptelee  28408  ausgrusgrb  28680  nbuhgr2vtx1edgblem  28863  nbgrsym  28875  isuvtx  28907  2wlkdlem6  29440  frcond1  29774  n4cyclfrgr  29799  shlesb1i  30894  mdsldmd1i  31839  csmdsymi  31842  lfuhgr  34394  2cycl2d  34416  dfon2lem3  35049  dfon2lem7  35053  filnetlem4  35569  ptrecube  36791  poimirlem30  36821  idinxpssinxp2  37490  cossssid2  37641  symrefref2  37736  redundeq1  37802  funALTVfun  37871  disjxrn  37919  omabs2  42384  undmrnresiss  42657  clcnvlem  42676  cnvtrrel  42723  brtrclfv2  42780  dfhe3  42828  dffrege76  42992  mnurndlem1  43342  ssabf  44091  rabssf  44110  imassmpt  44266  setrec2  47828