Theorem sseq1i 3629

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

Syntax hints:   ↔ wb 196   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  eqsstri  3635  syl5eqss  3649  ssab  3672  rabss  3679  uniiunlem  3691  prssg  4350  prssOLD  4352  sstp  4367  tpss  4368  iunss  4561  pwtr  4921  iunopeqop  4981  pwssun  5020  cores2  5648  sspred  5688  dffun2  5898  sbcfg  6043  idref  6499  ovmptss  7258  fnsuppres  7322  ordgt0ge1  7577  omopthlem1  7735  trcl  8604  rankbnd  8731  rankbnd2  8732  rankc1  8733  dfac12a  8970  fin23lem34  9168  axdc2lem  9270  alephval2  9394  indpi  9729  fsuppmapnn0fiublem  12789  0ram  15724  mreacs  16319  lsslinds  20170  2ndcctbss  21258  xkoinjcn  21490  restmetu  22375  xrlimcnp  24695  mptelee  25775  ausgrusgrb  26060  nbuhgr2vtx1edgblem  26247  nbgrsym  26265  isuvtxa  26295  2wlkdlem6  26827  frcond1  27130  n4cyclfrgr  27155  shlesb1i  28245  mdsldmd1i  29190  csmdsymi  29193  dfon2lem3  31690  dfon2lem7  31694  trpredmintr  31731  filnetlem4  32376  ptrecube  33409  poimirlem30  33439  idinxpssinxp2  34089  undmrnresiss  37910  clcnvlem  37930  ss2iundf  37951  cnvtrrel  37962  brtrclfv2  38019  rp-imass  38065  dfhe3  38069  dffrege76  38233  iunssf  39263  ssabf  39280  rabssf  39302  imassmpt  39481  setrec2  42442