Theorem sseq1i 3906

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

Syntax hints:   ↔ wb 209   = wceq 1542   ⊆ wss 3844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-v 3401  df-in 3851  df-ss 3861

This theorem is referenced by:  eqsstri  3912  eqsstrid  3926  ssab  3952  rabss  3962  uniiunlem  3976  prssg  4708  sstp  4723  tpss  4724  iunssf  4931  iunss  4932  pwtr  5312  iunopeqop  5379  pwssun  5426  cores2  6093  resssxp  6103  sspred  6138  dffun2  6350  sbcfg  6503  idref  6921  ovmptss  7817  fnsuppres  7889  ordgt0ge1  8156  omopthlem1  8316  trcl  9246  rankbnd  9373  rankbnd2  9374  rankc1  9375  dfac12a  9651  fin23lem34  9849  axdc2lem  9951  alephval2  10075  indpi  10410  fsuppmapnn0fiublem  13452  0ram  16459  mreacs  17035  lsslinds  20650  2ndcctbss  22209  xkoinjcn  22441  restmetu  23326  xrlimcnp  25709  mptelee  26844  ausgrusgrb  27113  nbuhgr2vtx1edgblem  27296  nbgrsym  27308  isuvtx  27340  2wlkdlem6  27872  frcond1  28206  n4cyclfrgr  28231  shlesb1i  29324  mdsldmd1i  30269  csmdsymi  30272  lfuhgr  32653  2cycl2d  32675  dfon2lem3  33338  dfon2lem7  33342  trpredmintr  33378  frrlem7  33452  filnetlem4  34216  ptrecube  35423  poimirlem30  35453  idinxpssinxp2  36099  cossssid2  36232  symrefref2  36323  redundeq1  36388  funALTVfun  36455  disjxrn  36501  undmrnresiss  40780  clcnvlem  40799  ss2iundf  40836  cnvtrrel  40847  brtrclfv2  40904  dfhe3  40952  dffrege76  41116  mnurndlem1  41464  ssabf  42211  rabssf  42229  imassmpt  42370  setrec2  45884