Theorem sseq1i 3975

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  eqsstrid  3985  eqsstri  3993  ssab  4027  rabss  4035  uniiunlem  4050  prssg  4783  sstp  4800  tpss  4801  iunssf  5008  iunss  5009  pwtr  5412  iunopeqop  5481  pwssun  5530  imadifssran  6124  cores2  6232  resssxp  6243  sspred  6283  dffun2OLDOLD  6523  sbcfg  6686  idref  7118  ovmptss  8072  fnsuppres  8170  frrlem7  8271  ordgt0ge1  8457  omopthlem1  8623  naddasslem1  8658  naddasslem2  8659  dmttrcl  9674  trcl  9681  rankbnd  9821  rankbnd2  9822  rankc1  9823  dfac12a  10102  fin23lem34  10299  axdc2lem  10401  alephval2  10525  indpi  10860  fsuppmapnn0fiublem  13955  prodeq1i  15882  0ram  16991  mreacs  17619  lsslinds  21740  2ndcctbss  23342  xkoinjcn  23574  restmetu  24458  xrlimcnp  26878  mptelee  28822  ausgrusgrb  29092  nbuhgr2vtx1edgblem  29278  nbgrsym  29290  isuvtx  29322  2wlkdlem6  29861  frcond1  30195  n4cyclfrgr  30220  shlesb1i  31315  mdsldmd1i  32260  csmdsymi  32263  tpssg  32466  lfuhgr  35105  2cycl2d  35126  dfon2lem3  35773  dfon2lem7  35777  cbvprodvw2  36235  filnetlem4  36369  ptrecube  37614  poimirlem30  37644  idinxpssinxp2  38306  cossssid2  38459  symrefref2  38554  redundeq1  38620  funALTVfun  38690  disjxrn  38738  omabs2  43321  undmrnresiss  43593  clcnvlem  43612  cnvtrrel  43659  brtrclfv2  43716  dfhe3  43764  dffrege76  43928  mnurndlem1  44270  ssabf  45094  rabssf  45113  imassmpt  45256  clnbgrsym  47838  sclnbgrelself  47848  setrec2  49684