Theorem sseq1i 3997

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

Syntax hints:   ↔ wb 208   = wceq 1537   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  eqsstri  4003  eqsstrid  4017  ssab  4043  rabss  4050  uniiunlem  4063  prssg  4754  sstp  4769  tpss  4770  iunss  4971  pwtr  5347  iunopeqop  5413  pwssun  5458  cores2  6114  sspred  6158  dffun2  6367  sbcfg  6514  idref  6910  ovmptss  7790  fnsuppres  7859  ordgt0ge1  8124  omopthlem1  8284  trcl  9172  rankbnd  9299  rankbnd2  9300  rankc1  9301  dfac12a  9576  fin23lem34  9770  axdc2lem  9872  alephval2  9996  indpi  10331  fsuppmapnn0fiublem  13361  0ram  16358  mreacs  16931  lsslinds  20977  2ndcctbss  22065  xkoinjcn  22297  restmetu  23182  xrlimcnp  25548  mptelee  26683  ausgrusgrb  26952  nbuhgr2vtx1edgblem  27135  nbgrsym  27147  isuvtx  27179  2wlkdlem6  27712  frcond1  28047  n4cyclfrgr  28072  shlesb1i  29165  mdsldmd1i  30110  csmdsymi  30113  lfuhgr  32366  2cycl2d  32388  dfon2lem3  33032  dfon2lem7  33036  trpredmintr  33072  frrlem7  33131  filnetlem4  33731  ptrecube  34894  poimirlem30  34924  idinxpssinxp2  35577  cossssid2  35710  symrefref2  35801  redundeq1  35866  funALTVfun  35933  disjxrn  35979  undmrnresiss  39971  clcnvlem  39990  ss2iundf  40011  cnvtrrel  40022  brtrclfv2  40079  rp-imass  40124  dfhe3  40128  dffrege76  40292  mnurndlem1  40624  iunssf  41359  ssabf  41373  rabssf  41392  imassmpt  41544  setrec2  44805