Theorem sseq1i 3941

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  eqsstrid  3951  eqsstri  3959  ssab  3991  rabss  3998  uniiunlem  4015  prssg  4778  sstp  4794  tpss  4795  iunssfOLD  5005  iunssOLD  5007  pwtr  5424  iunopeqop  5498  iunopeqopOLD  5499  pwssun  5547  cnvimassrndm  6091  imadifssranOLD  6215  imadifssranOLDOLD  6216  cores2  6274  resssxp  6290  sspred  6331  sbcfg  6729  idref  7173  ovmptss  8129  ovmptssOLD  8130  fnsuppres  8236  frrlem7  8338  ordgt0ge1  8529  omopthlem1  8696  naddasslem1  8732  naddasslem2  8733  dmttrcl  9749  trcl  9756  rankbnd  9912  rankbnd2  9913  rankc1  9914  setrec2  10004  dfac12a  10254  fin23lem34  10451  alephval2  10684  indpi  11019  fsuppmapnn0fiublem  14160  prodeq1i  16114  0ram  17227  mreacs  17861  lsslinds  22167  2ndcctbss  23804  xkoinjcn  24036  restmetu  24919  xrlimcnp  27326  mpteleeOLD  29503  lfuhgr  29756  ausgrusgrb  29776  nbuhgr2vtx1edgblem  29962  nbgrsym  29974  isuvtx  30006  2wlkdlem6  30550  frcond1  30897  n4cyclfrgr  30922  shlesb1i  32018  mdsldmd1i  32963  csmdsymi  32966  tpssg  33205  0elscott  35837  2cycl2d  36069  dfon2lem3  36725  dfon2lem7  36729  cbvprodvw2  37214  filnetlem4  37347  ptrecube  38730  poimirlem30  38760  idinxpssinxp2  39448  cossssid2  39682  symrefref2  39771  redundeq1  39837  funALTVfun  39907  disjxrn  39970  omabs2  44526  undmrnresiss  44796  clcnvlem  44815  cnvtrrel  44862  brtrclfv2  44919  dfhe3  44967  dffrege76  45131  mnurndlem1  45457  ssabf  46320  rabssf  46339  imassmpt  46479  clnbgrsym  49141  sclnbgrelself  49151