Theorem sseq1i 3964

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

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

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 2709

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

This theorem is referenced by:  eqsstrid  3974  eqsstri  3982  ssab  4017  rabss  4024  uniiunlem  4041  prssg  4777  sstp  4794  tpss  4795  iunssfOLD  5001  iunssOLD  5003  pwtr  5407  iunopeqop  5477  pwssun  5524  imadifssran  6117  cores2  6226  resssxp  6236  sspred  6276  sbcfg  6668  idref  7101  ovmptss  8045  fnsuppres  8143  frrlem7  8244  ordgt0ge1  8430  omopthlem1  8597  naddasslem1  8632  naddasslem2  8633  dmttrcl  9642  trcl  9649  rankbnd  9792  rankbnd2  9793  rankc1  9794  dfac12a  10071  fin23lem34  10268  alephval2  10495  indpi  10830  fsuppmapnn0fiublem  13925  prodeq1i  15851  0ram  16960  mreacs  17593  lsslinds  21798  2ndcctbss  23411  xkoinjcn  23643  restmetu  24526  xrlimcnp  26946  mpteleeOLD  28980  ausgrusgrb  29250  nbuhgr2vtx1edgblem  29436  nbgrsym  29448  isuvtx  29480  2wlkdlem6  30016  frcond1  30353  n4cyclfrgr  30378  shlesb1i  31473  mdsldmd1i  32418  csmdsymi  32421  tpssg  32623  lfuhgr  35331  2cycl2d  35352  dfon2lem3  35996  dfon2lem7  36000  cbvprodvw2  36460  filnetlem4  36594  ptrecube  37865  poimirlem30  37895  idinxpssinxp2  38569  cossssid2  38803  symrefref2  38892  redundeq1  38958  funALTVfun  39028  disjxrn  39091  omabs2  43683  undmrnresiss  43954  clcnvlem  43973  cnvtrrel  44020  brtrclfv2  44077  dfhe3  44125  dffrege76  44289  mnurndlem1  44631  ssabf  45453  rabssf  45472  imassmpt  45614  clnbgrsym  48192  sclnbgrelself  48202  setrec2  50048