Theorem sseq2i 3916

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

Syntax hints:   ↔ wb 209   = wceq 1543   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  sseqtri  3923  sseqtrdi  3937  abss  3960  ssrab  3972  ssindif0  4364  difcom  4386  ssunsn2  4726  ssunpr  4731  sspr  4732  sstp  4733  ssintrab  4868  iunpwss  5001  propssopi  5376  dffun2  6368  ssimaex  6774  elpwun  7532  ssfi  8829  frfi  8894  alephislim  9662  cardaleph  9668  fin1a2lem12  9990  zornn0g  10084  ssxr  10867  nnwo  12474  isstruct  16679  issubm  18184  grpissubg  18517  islinds  20725  basdif0  21804  tgdif0  21843  cmpsublem  22250  cmpsub  22251  hauscmplem  22257  2ndcctbss  22306  fbncp  22690  cnextfval  22913  eltsms  22984  reconn  23679  cmssmscld  24201  axcontlem3  27011  axcontlem4  27012  umgredg  27183  nbuhgr  27385  uhgrvd00  27576  vtxdginducedm1  27585  chsscon1i  29497  hatomistici  30397  chirredlem4  30428  atabs2i  30437  mdsymlem1  30438  mdsymlem3  30440  mdsymlem6  30443  mdsymlem8  30445  dmdbr5ati  30457  iundifdif  30575  nocvxminlem  33658  nocvxmin  33659  poimir  35496  ismblfin  35504  cossssid2  36272  ntrk0kbimka  41267  ntrclsk3  41298  ntrneicls11  41318  abssf  42276  ssrabf  42278  stoweidlem57  43216  ovnsubadd  43728  ovnovollem3  43814  issubmgm  44959  linccl  45371  lincdifsn  45381