Theorem sseq2i 3946

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

Syntax hints:   ↔ wb 205   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sseqtri  3953  sseqtrdi  3967  abss  3990  ssrab  4002  ssindif0  4394  difcom  4416  ssunsn2  4757  ssunpr  4762  sspr  4763  sstp  4764  ssintrab  4899  iunpwss  5032  propssopi  5416  dffun2  6428  ssimaex  6835  elpwun  7597  ssfi  8918  frfi  8989  alephislim  9770  cardaleph  9776  fin1a2lem12  10098  zornn0g  10192  ssxr  10975  nnwo  12582  isstruct  16781  issubm  18357  grpissubg  18690  islinds  20926  basdif0  22011  tgdif0  22050  cmpsublem  22458  cmpsub  22459  hauscmplem  22465  2ndcctbss  22514  fbncp  22898  cnextfval  23121  eltsms  23192  reconn  23897  cmssmscld  24419  axcontlem3  27237  axcontlem4  27238  umgredg  27411  nbuhgr  27613  uhgrvd00  27804  vtxdginducedm1  27813  chsscon1i  29725  hatomistici  30625  chirredlem4  30656  atabs2i  30665  mdsymlem1  30666  mdsymlem3  30668  mdsymlem6  30671  mdsymlem8  30673  dmdbr5ati  30685  iundifdif  30803  nocvxminlem  33899  nocvxmin  33900  poimir  35737  ismblfin  35745  cossssid2  36513  ntrk0kbimka  41538  ntrclsk3  41569  ntrneicls11  41589  abssf  42551  ssrabf  42553  stoweidlem57  43488  ovnsubadd  44000  ovnovollem3  44086  issubmgm  45231  linccl  45643  lincdifsn  45653