Theorem sseq2i 3963

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

Syntax hints:   ↔ wb 206   = wceq 1541   ⊆ wss 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728  df-ss 3918

This theorem is referenced by:  sseqtrdi  3974  sseqtri  3982  abss  4014  ssrab  4023  ssindif0  4416  difcom  4441  ssunsn2  4783  ssunpr  4790  sspr  4791  sstp  4792  ssintrab  4926  iunpwss  5062  propssopi  5456  f1imadifssran  6578  ssimaex  6919  elpwun  7714  ssfi  9097  frfi  9185  alephislim  9993  cardaleph  9999  fin1a2lem12  10321  zornn0g  10415  ssxr  11202  nnwo  12826  isstruct  17079  issubmgm  18627  issubm  18728  grpissubg  19076  issubrng  20480  cntzsubrng  20500  islinds  21764  basdif0  22897  tgdif0  22936  cmpsublem  23343  cmpsub  23344  hauscmplem  23350  2ndcctbss  23399  fbncp  23783  cnextfval  24006  eltsms  24077  reconn  24773  cmssmscld  25306  nobdaymin  27749  nocvxminlem  27750  axcontlem3  29039  axcontlem4  29040  umgredg  29211  nbuhgr  29416  uhgrvd00  29608  vtxdginducedm1  29617  chsscon1i  31537  hatomistici  32437  chirredlem4  32468  atabs2i  32477  mdsymlem1  32478  mdsymlem3  32480  mdsymlem6  32483  mdsymlem8  32485  dmdbr5ati  32497  iundifdif  32637  poimir  37854  ismblfin  37862  cossssid2  38731  ntrk0kbimka  44280  ntrclsk3  44311  ntrneicls11  44331  wfaxrep  45235  wfaxsep  45236  abssf  45356  ssrabf  45358  stoweidlem57  46301  ovnsubadd  46816  ovnovollem3  46902  grlimedgclnbgr  48241  linccl  48660  lincdifsn  48670