Theorem sseq1i 3968

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ss 3925

This theorem is used by:  eqsstrid  3978  eqsstri  3986  ssab  4020  rabss  4027  uniiunlem  4044  prssg  4790  sstp  4806  tpss  4807  iunssfOLD  5013  iunssOLD  5015  pwtr  5438  iunopeqop  5509  iunopeqopOLD  5510  pwssun  5558  imadifssran  6207  imadifssranOLD  6208  cores2  6266  resssxp  6277  sspred  6318  sbcfg  6710  idref  7149  ovmptss  8097  fnsuppres  8196  frrlem7  8298  ordgt0ge1  8487  omopthlem1  8654  naddasslem1  8690  naddasslem2  8691  dmttrcl  9700  trcl  9707  rankbnd  9850  rankbnd2  9851  rankc1  9852  dfac12a  10151  fin23lem34  10348  alephval2  10575  indpi  10910  fsuppmapnn0fiublem  14046  prodeq1i  15996  0ram  17105  mreacs  17739  lsslinds  22018  2ndcctbss  23649  xkoinjcn  23881  restmetu  24764  xrlimcnp  27170  mpteleeOLD  29282  ausgrusgrb  29552  nbuhgr2vtx1edgblem  29738  nbgrsym  29750  isuvtx  29782  2wlkdlem6  30317  frcond1  30654  n4cyclfrgr  30679  shlesb1i  31775  mdsldmd1i  32720  csmdsymi  32723  tpssg  32920  lfuhgr  35630  2cycl2d  35651  dfon2lem3  36295  dfon2lem7  36299  cbvprodvw2  36799  filnetlem4  36932  ptrecube  38311  poimirlem30  38341  idinxpssinxp2  39013  cossssid2  39247  symrefref2  39336  redundeq1  39402  funALTVfun  39472  disjxrn  39535  omabs2  44099  undmrnresiss  44370  clcnvlem  44389  cnvtrrel  44436  brtrclfv2  44493  dfhe3  44541  dffrege76  44705  mnurndlem1  45031  ssabf  45858  rabssf  45877  imassmpt  46017  clnbgrsym  48643  sclnbgrelself  48653  setrec2  50513