Theorem sseq2i 4008

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ss 3963

This theorem is referenced by:  sseqtri  4015  sseqtrdi  4029  abss  4056  ssrab  4066  ssindif0  4458  difcom  4483  ssunsn2  4826  ssunpr  4833  sspr  4834  sstp  4835  ssintrab  4971  iunpwss  5107  propssopi  5506  dffun2OLDOLD  6558  ssimaex  6979  elpwun  7769  ssfi  9204  frfi  9315  alephislim  10119  cardaleph  10125  fin1a2lem12  10445  zornn0g  10539  ssxr  11324  nnwo  12943  isstruct  17149  issubmgm  18690  issubm  18788  grpissubg  19136  issubrng  20525  cntzsubrng  20545  islinds  21803  basdif0  22944  tgdif0  22983  cmpsublem  23391  cmpsub  23392  hauscmplem  23398  2ndcctbss  23447  fbncp  23831  cnextfval  24054  eltsms  24125  reconn  24832  cmssmscld  25366  nocvxminlem  27804  nocvxmin  27805  axcontlem3  28897  axcontlem4  28898  umgredg  29071  nbuhgr  29276  uhgrvd00  29468  vtxdginducedm1  29477  chsscon1i  31392  hatomistici  32292  chirredlem4  32323  atabs2i  32332  mdsymlem1  32333  mdsymlem3  32335  mdsymlem6  32338  mdsymlem8  32340  dmdbr5ati  32352  iundifdif  32483  poimir  37367  ismblfin  37375  cossssid2  38179  ntrk0kbimka  43743  ntrclsk3  43774  ntrneicls11  43794  abssf  44750  ssrabf  44752  stoweidlem57  45714  ovnsubadd  46229  ovnovollem3  46315  linccl  47833  lincdifsn  47843