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  28255  axcontlem4  28256  umgredg  28429  nbuhgr  28631  uhgrvd00  28822  vtxdginducedm1  28831  chsscon1i  30746  hatomistici  31646  chirredlem4  31677  atabs2i  31686  mdsymlem1  31687  mdsymlem3  31689  mdsymlem6  31692  mdsymlem8  31694  dmdbr5ati  31706  iundifdif  31825  poimir  36569  ismblfin  36577  cossssid2  37386  ntrk0kbimka  42838  ntrclsk3  42869  ntrneicls11  42889  abssf  43849  ssrabf  43851  stoweidlem57  44821  ovnsubadd  45336  ovnovollem3  45422  issubmgm  46607  issubrng  46774  cntzsubrng  46794  linccl  47143  lincdifsn  47153