Theorem sseq1i 3987

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

Syntax hints:   ↔ wb 206   = wceq 1540   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943

This theorem is referenced by:  eqsstrid  3997  eqsstri  4005  ssab  4039  rabss  4047  uniiunlem  4062  prssg  4795  sstp  4812  tpss  4813  iunssf  5020  iunss  5021  pwtr  5427  iunopeqop  5496  pwssun  5545  imadifssran  6140  cores2  6248  resssxp  6259  sspred  6299  dffun2OLDOLD  6543  sbcfg  6704  idref  7136  ovmptss  8092  fnsuppres  8190  frrlem7  8291  ordgt0ge1  8505  omopthlem1  8671  naddasslem1  8706  naddasslem2  8707  dmttrcl  9735  trcl  9742  rankbnd  9882  rankbnd2  9883  rankc1  9884  dfac12a  10163  fin23lem34  10360  axdc2lem  10462  alephval2  10586  indpi  10921  fsuppmapnn0fiublem  14008  prodeq1i  15932  0ram  17040  mreacs  17670  lsslinds  21791  2ndcctbss  23393  xkoinjcn  23625  restmetu  24509  xrlimcnp  26930  mptelee  28874  ausgrusgrb  29144  nbuhgr2vtx1edgblem  29330  nbgrsym  29342  isuvtx  29374  2wlkdlem6  29913  frcond1  30247  n4cyclfrgr  30272  shlesb1i  31367  mdsldmd1i  32312  csmdsymi  32315  tpssg  32518  lfuhgr  35140  2cycl2d  35161  dfon2lem3  35803  dfon2lem7  35807  cbvprodvw2  36265  filnetlem4  36399  ptrecube  37644  poimirlem30  37674  idinxpssinxp2  38336  cossssid2  38486  symrefref2  38581  redundeq1  38647  funALTVfun  38716  disjxrn  38764  omabs2  43356  undmrnresiss  43628  clcnvlem  43647  cnvtrrel  43694  brtrclfv2  43751  dfhe3  43799  dffrege76  43963  mnurndlem1  44305  ssabf  45124  rabssf  45143  imassmpt  45286  clnbgrsym  47851  sclnbgrelself  47861  setrec2  49559