Theorem sseq1i 4011

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

Syntax hints:   ↔ wb 205   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  eqsstri  4017  eqsstrid  4031  ssab  4059  rabss  4070  uniiunlem  4085  prssg  4823  sstp  4838  tpss  4839  iunssf  5048  iunss  5049  pwtr  5453  iunopeqop  5522  pwssun  5572  cores2  6259  resssxp  6270  sspred  6310  dffun2OLDOLD  6556  sbcfg  6716  idref  7144  ovmptss  8079  fnsuppres  8176  frrlem7  8277  ordgt0ge1  8493  omopthlem1  8658  naddasslem1  8693  naddasslem2  8694  dmttrcl  9716  trcl  9723  rankbnd  9863  rankbnd2  9864  rankc1  9865  dfac12a  10143  fin23lem34  10341  axdc2lem  10443  alephval2  10567  indpi  10902  fsuppmapnn0fiublem  13955  0ram  16953  mreacs  17602  lsslinds  21386  2ndcctbss  22959  xkoinjcn  23191  restmetu  24079  xrlimcnp  26473  mptelee  28184  ausgrusgrb  28456  nbuhgr2vtx1edgblem  28639  nbgrsym  28651  isuvtx  28683  2wlkdlem6  29216  frcond1  29550  n4cyclfrgr  29575  shlesb1i  30670  mdsldmd1i  31615  csmdsymi  31618  lfuhgr  34139  2cycl2d  34161  dfon2lem3  34788  dfon2lem7  34792  filnetlem4  35314  ptrecube  36536  poimirlem30  36566  idinxpssinxp2  37235  cossssid2  37386  symrefref2  37481  redundeq1  37547  funALTVfun  37616  disjxrn  37664  omabs2  42130  undmrnresiss  42403  clcnvlem  42422  cnvtrrel  42469  brtrclfv2  42526  dfhe3  42574  dffrege76  42738  mnurndlem1  43088  ssabf  43837  rabssf  43856  imassmpt  44015  setrec2  47788