Theorem sseq1i 4008

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

Syntax hints:   ↔ wb 205   = wceq 1542   ⊆ wss 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3953  df-ss 3963

This theorem is referenced by:  eqsstri  4014  eqsstrid  4028  ssab  4056  rabss  4067  uniiunlem  4082  prssg  4820  sstp  4835  tpss  4836  iunssf  5045  iunss  5046  pwtr  5450  iunopeqop  5519  pwssun  5569  cores2  6254  resssxp  6265  sspred  6305  dffun2OLDOLD  6551  sbcfg  6711  idref  7138  ovmptss  8073  fnsuppres  8170  frrlem7  8271  ordgt0ge1  8487  omopthlem1  8653  naddasslem1  8688  naddasslem2  8689  dmttrcl  9711  trcl  9718  rankbnd  9858  rankbnd2  9859  rankc1  9860  dfac12a  10138  fin23lem34  10336  axdc2lem  10438  alephval2  10562  indpi  10897  fsuppmapnn0fiublem  13950  0ram  16948  mreacs  17597  lsslinds  21369  2ndcctbss  22940  xkoinjcn  23172  restmetu  24060  xrlimcnp  26452  mptelee  28132  ausgrusgrb  28404  nbuhgr2vtx1edgblem  28587  nbgrsym  28599  isuvtx  28631  2wlkdlem6  29164  frcond1  29498  n4cyclfrgr  29523  shlesb1i  30616  mdsldmd1i  31561  csmdsymi  31564  lfuhgr  34045  2cycl2d  34067  dfon2lem3  34694  dfon2lem7  34698  filnetlem4  35203  ptrecube  36425  poimirlem30  36455  idinxpssinxp2  37124  cossssid2  37275  symrefref2  37370  redundeq1  37436  funALTVfun  37505  disjxrn  37553  omabs2  42014  undmrnresiss  42287  clcnvlem  42306  cnvtrrel  42353  brtrclfv2  42410  dfhe3  42458  dffrege76  42622  mnurndlem1  42972  ssabf  43721  rabssf  43740  imassmpt  43901  setrec2  47641