Theorem sseq1i 3823

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

Syntax hints:   ↔ wb 198   = wceq 1653   ⊆ wss 3767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-in 3774  df-ss 3781

This theorem is referenced by:  eqsstri  3829  syl5eqss  3843  ssab  3866  rabss  3873  uniiunlem  3886  prssg  4536  sstp  4551  tpss  4552  iunss  4749  pwtr  5110  iunopeqop  5175  pwssun  5214  cores2  5865  sspred  5904  dffun2  6109  sbcfg  6252  idref  6637  ovmptss  7493  fnsuppres  7558  ordgt0ge1  7815  omopthlem1  7973  trcl  8852  rankbnd  8979  rankbnd2  8980  rankc1  8981  dfac12a  9256  fin23lem34  9454  axdc2lem  9556  alephval2  9680  indpi  10015  fsuppmapnn0fiublem  13040  0ram  16053  mreacs  16629  lsslinds  20491  2ndcctbss  21583  xkoinjcn  21815  restmetu  22699  xrlimcnp  25043  mptelee  26123  ausgrusgrb  26392  nbuhgr2vtx1edgblem  26580  nbgrsym  26596  nbgrsymOLD  26597  isuvtx  26632  isuvtxaOLD  26633  2wlkdlem6  27211  frcond1  27606  n4cyclfrgr  27631  shlesb1i  28761  mdsldmd1i  29706  csmdsymi  29709  dfon2lem3  32193  dfon2lem7  32197  trpredmintr  32234  filnetlem4  32879  ptrecube  33889  poimirlem30  33919  idinxpssinxp2  34574  cossssid2  34703  symrefref2  34794  redeq1  34855  undmrnresiss  38680  clcnvlem  38700  ss2iundf  38721  cnvtrrel  38732  brtrclfv2  38789  rp-imass  38834  dfhe3  38838  dffrege76  39002  iunssf  40009  ssabf  40026  rabssf  40047  imassmpt  40215  setrec2  43228