Theorem sseq2i 3967

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  sseqtrdi  3978  sseqtri  3986  abss  4017  ssrab  4026  ssindif0  4424  difcom  4451  ssunsn2  4795  ssunpr  4801  sspr  4802  sstp  4803  ssintrab  4938  iunpwss  5075  propssopi  5493  ssimaex  6970  elpwun  7770  ssfi  9160  frfi  9248  alephislim  10079  cardaleph  10085  fin1a2lem12  10406  zornn0g  10500  ssxr  11290  nnwo  12948  isstruct  17229  issubmgm  18781  issubm  18884  grpissubg  19236  issubrng  20675  cntzsubrng  20695  rspvalint  21398  islinds  21988  basdif0  23139  tgdif0  23178  cmpsublem  23585  cmpsub  23586  hauscmplem  23592  2ndcctbss  23641  fbncp  24025  cnextfval  24248  eltsms  24319  reconn  25015  cmssmscld  25538  nobdaymin  27975  nocvxminlem  27976  axcontlem3  29345  axcontlem4  29346  umgredg  29517  nbuhgr  29722  uhgrvd00  29913  vtxdginducedm1  29922  chsscon1i  31843  hatomistici  32743  chirredlem4  32774  atabs2i  32783  mdsymlem1  32784  mdsymlem3  32786  mdsymlem6  32789  mdsymlem8  32791  dmdbr5ati  32803  iundifdif  32936  poimir  38337  ismblfin  38345  cossssid2  39240  ntrk0kbimka  44798  ntrclsk3  44829  ntrneicls11  44849  wfaxrep  45736  wfaxsep  45737  abssf  45863  ssrabf  45865  stoweidlem57  46804  ovnsubadd  47319  ovnovollem3  47405  grlimedgclnbgr  48793  linccl  49227  lincdifsn  49237