Theorem sseq1i 3778

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

Syntax hints:   ↔ wb 196   = wceq 1631   ⊆ wss 3723

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737

This theorem is referenced by:  eqsstri  3784  syl5eqss  3798  ssab  3821  rabss  3828  uniiunlem  3841  prssg  4485  sstp  4500  tpss  4501  iunss  4695  pwtr  5049  iunopeqop  5114  pwssun  5153  cores2  5792  sspred  5831  dffun2  6041  sbcfg  6183  idref  6642  ovmptss  7409  fnsuppres  7474  ordgt0ge1  7731  omopthlem1  7889  trcl  8768  rankbnd  8895  rankbnd2  8896  rankc1  8897  dfac12a  9172  fin23lem34  9370  axdc2lem  9472  alephval2  9596  indpi  9931  fsuppmapnn0fiublem  12997  0ram  15931  mreacs  16526  lsslinds  20387  2ndcctbss  21479  xkoinjcn  21711  restmetu  22595  xrlimcnp  24916  mptelee  25996  ausgrusgrb  26282  nbuhgr2vtx1edgblem  26470  nbgrsym  26486  nbgrsymOLD  26487  isuvtx  26522  isuvtxaOLD  26523  2wlkdlem6  27078  frcond1  27448  n4cyclfrgr  27473  shlesb1i  28585  mdsldmd1i  29530  csmdsymi  29533  dfon2lem3  32026  dfon2lem7  32030  trpredmintr  32067  filnetlem4  32713  ptrecube  33742  poimirlem30  33772  idinxpssinxp2  34432  cossssid2  34560  symrefref2  34651  undmrnresiss  38436  clcnvlem  38456  ss2iundf  38477  cnvtrrel  38488  brtrclfv2  38545  rp-imass  38591  dfhe3  38595  dffrege76  38759  iunssf  39784  ssabf  39801  rabssf  39823  imassmpt  39999  setrec2  42970