Theorem sseq2i 3976

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

Syntax hints:   ↔ wb 206   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  sseqtrdi  3987  sseqtri  3995  abss  4026  ssrab  4036  ssindif0  4427  difcom  4452  ssunsn2  4791  ssunpr  4798  sspr  4799  sstp  4800  ssintrab  4935  iunpwss  5071  propssopi  5468  dffun2OLDOLD  6523  f1imadifssran  6602  ssimaex  6946  elpwun  7745  ssfi  9137  frfi  9232  alephislim  10036  cardaleph  10042  fin1a2lem12  10364  zornn0g  10458  ssxr  11243  nnwo  12872  isstruct  17122  issubmgm  18629  issubm  18730  grpissubg  19078  issubrng  20456  cntzsubrng  20476  islinds  21718  basdif0  22840  tgdif0  22879  cmpsublem  23286  cmpsub  23287  hauscmplem  23293  2ndcctbss  23342  fbncp  23726  cnextfval  23949  eltsms  24020  reconn  24717  cmssmscld  25250  nocvxminlem  27689  nocvxmin  27690  axcontlem3  28893  axcontlem4  28894  umgredg  29065  nbuhgr  29270  uhgrvd00  29462  vtxdginducedm1  29471  chsscon1i  31391  hatomistici  32291  chirredlem4  32322  atabs2i  32331  mdsymlem1  32332  mdsymlem3  32334  mdsymlem6  32337  mdsymlem8  32339  dmdbr5ati  32351  iundifdif  32491  poimir  37647  ismblfin  37655  cossssid2  38459  ntrk0kbimka  44028  ntrclsk3  44059  ntrneicls11  44079  wfaxrep  44984  wfaxsep  44985  abssf  45106  ssrabf  45108  stoweidlem57  46055  ovnsubadd  46570  ovnovollem3  46656  linccl  48403  lincdifsn  48413