Theorem sseq1i 3621

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

Syntax hints:   ↔ wb 196   = wceq 1481   ⊆ wss 3567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-in 3574  df-ss 3581

This theorem is referenced by:  eqsstri  3627  syl5eqss  3641  ssab  3664  rabss  3671  uniiunlem  3683  prssg  4341  prssOLD  4343  sstp  4358  tpss  4359  iunss  4552  pwtr  4912  iunopeqop  4971  pwssun  5010  cores2  5636  sspred  5676  dffun2  5886  sbcfg  6030  idref  6484  ovmptss  7243  fnsuppres  7307  ordgt0ge1  7562  omopthlem1  7720  trcl  8589  rankbnd  8716  rankbnd2  8717  rankc1  8718  dfac12a  8955  fin23lem34  9153  axdc2lem  9255  alephval2  9379  indpi  9714  fsuppmapnn0fiublem  12772  0ram  15705  mreacs  16300  lsslinds  20151  2ndcctbss  21239  xkoinjcn  21471  restmetu  22356  xrlimcnp  24676  mptelee  25756  ausgrusgrb  26041  nbuhgr2vtx1edgblem  26228  nbgrsym  26246  isuvtxa  26276  2wlkdlem6  26808  frcond1  27110  n4cyclfrgr  27135  shlesb1i  28215  mdsldmd1i  29160  csmdsymi  29163  dfon2lem3  31664  dfon2lem7  31668  trpredmintr  31705  filnetlem4  32351  ptrecube  33380  poimirlem30  33410  undmrnresiss  37729  clcnvlem  37749  ss2iundf  37770  cnvtrrel  37781  brtrclfv2  37838  rp-imass  37885  dfhe3  37889  dffrege76  38053  iunssf  39083  ssabf  39100  rabssf  39122  imassmpt  39297  setrec2  42207