Theorem sseq2i 4012

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

Syntax hints:   ↔ wb 205   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sseqtri  4019  sseqtrdi  4033  abss  4058  ssrab  4071  ssindif0  4464  difcom  4489  ssunsn2  4831  ssunpr  4836  sspr  4837  sstp  4838  ssintrab  4976  iunpwss  5111  propssopi  5509  dffun2OLDOLD  6556  ssimaex  6977  elpwun  7756  ssfi  9173  frfi  9288  alephislim  10078  cardaleph  10084  fin1a2lem12  10406  zornn0g  10500  ssxr  11283  nnwo  12897  isstruct  17085  issubm  18684  grpissubg  19026  islinds  21364  basdif0  22456  tgdif0  22495  cmpsublem  22903  cmpsub  22904  hauscmplem  22910  2ndcctbss  22959  fbncp  23343  cnextfval  23566  eltsms  23637  reconn  24344  cmssmscld  24867  nocvxminlem  27279  nocvxmin  27280  axcontlem3  28224  axcontlem4  28225  umgredg  28398  nbuhgr  28600  uhgrvd00  28791  vtxdginducedm1  28800  chsscon1i  30715  hatomistici  31615  chirredlem4  31646  atabs2i  31655  mdsymlem1  31656  mdsymlem3  31658  mdsymlem6  31661  mdsymlem8  31663  dmdbr5ati  31675  iundifdif  31794  poimir  36521  ismblfin  36529  cossssid2  37338  ntrk0kbimka  42790  ntrclsk3  42821  ntrneicls11  42841  abssf  43801  ssrabf  43803  stoweidlem57  44773  ovnsubadd  45288  ovnovollem3  45374  issubmgm  46559  issubrng  46726  cntzsubrng  46746  linccl  47095  lincdifsn  47105