Theorem sseq1i 3950

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

Syntax hints:   ↔ wb 206   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  eqsstrid  3960  eqsstri  3968  ssab  4003  rabss  4010  uniiunlem  4027  prssg  4762  sstp  4779  tpss  4780  iunssfOLD  4986  iunssOLD  4988  pwtr  5404  iunopeqop  5475  iunopeqopOLD  5476  pwssun  5523  imadifssran  6115  cores2  6224  resssxp  6234  sspred  6274  sbcfg  6666  idref  7099  ovmptss  8043  fnsuppres  8141  frrlem7  8242  ordgt0ge1  8428  omopthlem1  8595  naddasslem1  8630  naddasslem2  8631  dmttrcl  9642  trcl  9649  rankbnd  9792  rankbnd2  9793  rankc1  9794  dfac12a  10071  fin23lem34  10268  alephval2  10495  indpi  10830  fsuppmapnn0fiublem  13952  prodeq1i  15881  0ram  16991  mreacs  17624  lsslinds  21811  2ndcctbss  23420  xkoinjcn  23652  restmetu  24535  xrlimcnp  26932  mpteleeOLD  28964  ausgrusgrb  29234  nbuhgr2vtx1edgblem  29420  nbgrsym  29432  isuvtx  29464  2wlkdlem6  29999  frcond1  30336  n4cyclfrgr  30361  shlesb1i  31457  mdsldmd1i  32402  csmdsymi  32405  tpssg  32607  lfuhgr  35300  2cycl2d  35321  dfon2lem3  35965  dfon2lem7  35969  cbvprodvw2  36429  filnetlem4  36563  ptrecube  37941  poimirlem30  37971  idinxpssinxp2  38645  cossssid2  38879  symrefref2  38968  redundeq1  39034  funALTVfun  39104  disjxrn  39167  omabs2  43760  undmrnresiss  44031  clcnvlem  44050  cnvtrrel  44097  brtrclfv2  44154  dfhe3  44202  dffrege76  44366  mnurndlem1  44708  ssabf  45530  rabssf  45549  imassmpt  45691  clnbgrsym  48314  sclnbgrelself  48324  setrec2  50170