Theorem sseq1i 4012

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

Syntax hints:   ↔ wb 206   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  eqsstrid  4022  eqsstri  4030  ssab  4064  rabss  4072  uniiunlem  4087  prssg  4819  sstp  4836  tpss  4837  iunssf  5044  iunss  5045  pwtr  5457  iunopeqop  5526  pwssun  5575  imadifssran  6171  cores2  6279  resssxp  6290  sspred  6330  dffun2OLDOLD  6573  sbcfg  6734  idref  7166  ovmptss  8118  fnsuppres  8216  frrlem7  8317  ordgt0ge1  8531  omopthlem1  8697  naddasslem1  8732  naddasslem2  8733  dmttrcl  9761  trcl  9768  rankbnd  9908  rankbnd2  9909  rankc1  9910  dfac12a  10189  fin23lem34  10386  axdc2lem  10488  alephval2  10612  indpi  10947  fsuppmapnn0fiublem  14031  prodeq1i  15952  0ram  17058  mreacs  17701  lsslinds  21851  2ndcctbss  23463  xkoinjcn  23695  restmetu  24583  xrlimcnp  27011  mptelee  28910  ausgrusgrb  29182  nbuhgr2vtx1edgblem  29368  nbgrsym  29380  isuvtx  29412  2wlkdlem6  29951  frcond1  30285  n4cyclfrgr  30310  shlesb1i  31405  mdsldmd1i  32350  csmdsymi  32353  lfuhgr  35123  2cycl2d  35144  dfon2lem3  35786  dfon2lem7  35790  cbvprodvw2  36248  filnetlem4  36382  ptrecube  37627  poimirlem30  37657  idinxpssinxp2  38319  cossssid2  38469  symrefref2  38564  redundeq1  38630  funALTVfun  38699  disjxrn  38747  omabs2  43345  undmrnresiss  43617  clcnvlem  43636  cnvtrrel  43683  brtrclfv2  43740  dfhe3  43788  dffrege76  43952  mnurndlem1  44300  ssabf  45105  rabssf  45124  imassmpt  45269  clnbgrsym  47824  sclnbgrelself  47834  setrec2  49214