Theorem sseq2i 3923

Description: An equality inference for the subclass relationship. (Contributed by NM, 30-Aug-1993.)

Hypothesis

Ref	Expression
sseq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
sseq2i	⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)

Proof of Theorem sseq2i

Step	Hyp	Ref	Expression
1		sseq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		sseq2 3920	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)

Syntax hints:   ↔ wb 207   = wceq 1525   ⊆ wss 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-in 3872  df-ss 3880

This theorem is referenced by:  sseqtri  3930  syl6sseq  3944  abss  3967  ssrab  3976  ssindif0  4333  difcom  4354  ssunsn2  4673  ssunpr  4678  sspr  4679  sstp  4680  ssintrab  4811  iunpwss  4934  propssopi  5296  dffun2  6242  ssimaex  6622  elpwun  7355  frfi  8616  alephislim  9362  cardaleph  9368  fin1a2lem12  9686  zornn0g  9780  ssxr  10563  nnwo  12166  isstruct  16329  issubm  17790  grpissubg  18057  islinds  20639  basdif0  21249  tgdif0  21288  cmpsublem  21695  cmpsub  21696  hauscmplem  21702  2ndcctbss  21751  fbncp  22135  cnextfval  22358  eltsms  22428  reconn  23123  cmssmscld  23640  axcontlem3  26439  axcontlem4  26440  umgredg  26610  nbuhgr  26812  uhgrvd00  27003  vtxdginducedm1  27012  chsscon1i  28926  hatomistici  29826  chirredlem4  29857  atabs2i  29866  mdsymlem1  29867  mdsymlem3  29869  mdsymlem6  29872  mdsymlem8  29874  dmdbr5ati  29886  iundifdif  30000  nocvxminlem  32858  nocvxmin  32859  poimir  34477  ismblfin  34485  cossssid2  35260  ntrk0kbimka  39895  ntrclsk3  39926  ntrneicls11  39946  abssf  40939  ssrabf  40942  stoweidlem57  41906  ovnsubadd  42418  ovnovollem3  42504  issubmgm  43560  linccl  43971  lincdifsn  43981