Theorem sseq1i 3954

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

Syntax hints:   ↔ wb 205   = wceq 1539   ⊆ wss 3892

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909

This theorem is referenced by:  eqsstri  3960  eqsstrid  3974  ssab  4000  rabss  4011  uniiunlem  4025  prssg  4758  sstp  4773  tpss  4774  iunssf  4981  iunss  4982  pwtr  5381  iunopeqop  5448  pwssun  5497  cores2  6177  resssxp  6188  sspred  6226  dffun2OLDOLD  6470  sbcfg  6628  idref  7050  ovmptss  7965  fnsuppres  8038  frrlem7  8139  ordgt0ge1  8354  omopthlem1  8520  dmttrcl  9527  trcl  9534  rankbnd  9674  rankbnd2  9675  rankc1  9676  dfac12a  9954  fin23lem34  10152  axdc2lem  10254  alephval2  10378  indpi  10713  fsuppmapnn0fiublem  13760  0ram  16770  mreacs  17416  lsslinds  21087  2ndcctbss  22655  xkoinjcn  22887  restmetu  23775  xrlimcnp  26167  mptelee  27312  ausgrusgrb  27584  nbuhgr2vtx1edgblem  27767  nbgrsym  27779  isuvtx  27811  2wlkdlem6  28345  frcond1  28679  n4cyclfrgr  28704  shlesb1i  29797  mdsldmd1i  30742  csmdsymi  30745  lfuhgr  33128  2cycl2d  33150  dfon2lem3  33810  dfon2lem7  33814  filnetlem4  34619  ptrecube  35825  poimirlem30  35855  idinxpssinxp2  36531  cossssid2  36682  symrefref2  36777  redundeq1  36843  funALTVfun  36912  disjxrn  36960  undmrnresiss  41425  clcnvlem  41444  cnvtrrel  41491  brtrclfv2  41548  dfhe3  41596  dffrege76  41760  mnurndlem1  42112  ssabf  42863  rabssf  42882  imassmpt  43031  setrec2  46645