Theorem sseq1i 3662

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

Syntax hints:   ↔ wb 196   = wceq 1523   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621

This theorem is referenced by:  eqsstri  3668  syl5eqss  3682  ssab  3705  rabss  3712  uniiunlem  3724  prssg  4382  prssOLD  4384  sstp  4399  tpss  4400  iunss  4593  pwtr  4951  iunopeqop  5010  pwssun  5049  cores2  5686  sspred  5726  dffun2  5936  sbcfg  6081  idref  6539  ovmptss  7303  fnsuppres  7367  ordgt0ge1  7622  omopthlem1  7780  trcl  8642  rankbnd  8769  rankbnd2  8770  rankc1  8771  dfac12a  9008  fin23lem34  9206  axdc2lem  9308  alephval2  9432  indpi  9767  fsuppmapnn0fiublem  12829  0ram  15771  mreacs  16366  lsslinds  20218  2ndcctbss  21306  xkoinjcn  21538  restmetu  22422  xrlimcnp  24740  mptelee  25820  ausgrusgrb  26105  nbuhgr2vtx1edgblem  26292  nbgrsym  26308  nbgrsymOLD  26309  isuvtx  26343  isuvtxaOLD  26344  2wlkdlem6  26896  frcond1  27246  n4cyclfrgr  27271  shlesb1i  28373  mdsldmd1i  29318  csmdsymi  29321  dfon2lem3  31814  dfon2lem7  31818  trpredmintr  31855  filnetlem4  32501  ptrecube  33539  poimirlem30  33569  idinxpssinxp2  34230  cossssid2  34358  symrefref2  34447  undmrnresiss  38227  clcnvlem  38247  ss2iundf  38268  cnvtrrel  38279  brtrclfv2  38336  rp-imass  38382  dfhe3  38386  dffrege76  38550  iunssf  39577  ssabf  39594  rabssf  39616  imassmpt  39795  setrec2  42767