Theorem sseq1i 3943

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

Syntax hints:   ↔ wb 209   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  eqsstri  3949  eqsstrid  3963  ssab  3989  rabss  3999  uniiunlem  4012  prssg  4712  sstp  4727  tpss  4728  iunssf  4931  iunss  4932  pwtr  5310  iunopeqop  5376  pwssun  5421  cores2  6079  resssxp  6089  sspred  6124  dffun2  6334  sbcfg  6485  idref  6885  ovmptss  7771  fnsuppres  7840  ordgt0ge1  8105  omopthlem1  8265  trcl  9154  rankbnd  9281  rankbnd2  9282  rankc1  9283  dfac12a  9559  fin23lem34  9757  axdc2lem  9859  alephval2  9983  indpi  10318  fsuppmapnn0fiublem  13353  0ram  16346  mreacs  16921  lsslinds  20520  2ndcctbss  22060  xkoinjcn  22292  restmetu  23177  xrlimcnp  25554  mptelee  26689  ausgrusgrb  26958  nbuhgr2vtx1edgblem  27141  nbgrsym  27153  isuvtx  27185  2wlkdlem6  27717  frcond1  28051  n4cyclfrgr  28076  shlesb1i  29169  mdsldmd1i  30114  csmdsymi  30117  lfuhgr  32477  2cycl2d  32499  dfon2lem3  33143  dfon2lem7  33147  trpredmintr  33183  frrlem7  33242  filnetlem4  33842  ptrecube  35057  poimirlem30  35087  idinxpssinxp2  35735  cossssid2  35868  symrefref2  35959  redundeq1  36024  funALTVfun  36091  disjxrn  36137  undmrnresiss  40304  clcnvlem  40323  ss2iundf  40360  cnvtrrel  40371  brtrclfv2  40428  dfhe3  40476  dffrege76  40640  mnurndlem1  40989  ssabf  41736  rabssf  41754  imassmpt  41902  setrec2  45225