Theorem sseq1i 3953

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

Syntax hints:   ↔ wb 205   = wceq 1541   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  eqsstri  3959  eqsstrid  3973  ssab  3999  rabss  4009  uniiunlem  4023  prssg  4757  sstp  4772  tpss  4773  iunssf  4978  iunss  4979  pwtr  5370  iunopeqop  5437  pwssun  5484  cores2  6160  resssxp  6170  sspred  6208  dffun2  6440  sbcfg  6594  idref  7012  ovmptss  7917  fnsuppres  7991  frrlem7  8092  ordgt0ge1  8303  omopthlem1  8463  dmttrcl  9440  trpredmintr  9461  trcl  9469  rankbnd  9610  rankbnd2  9611  rankc1  9612  dfac12a  9888  fin23lem34  10086  axdc2lem  10188  alephval2  10312  indpi  10647  fsuppmapnn0fiublem  13691  0ram  16702  mreacs  17348  lsslinds  21019  2ndcctbss  22587  xkoinjcn  22819  restmetu  23707  xrlimcnp  26099  mptelee  27244  ausgrusgrb  27516  nbuhgr2vtx1edgblem  27699  nbgrsym  27711  isuvtx  27743  2wlkdlem6  28275  frcond1  28609  n4cyclfrgr  28634  shlesb1i  29727  mdsldmd1i  30672  csmdsymi  30675  lfuhgr  33058  2cycl2d  33080  dfon2lem3  33740  dfon2lem7  33744  filnetlem4  34549  ptrecube  35756  poimirlem30  35786  idinxpssinxp2  36432  cossssid2  36565  symrefref2  36656  redundeq1  36721  funALTVfun  36788  disjxrn  36834  undmrnresiss  41165  clcnvlem  41184  ss2iundf  41220  cnvtrrel  41231  brtrclfv2  41288  dfhe3  41336  dffrege76  41500  mnurndlem1  41852  ssabf  42603  rabssf  42621  imassmpt  42763  setrec2  46353