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 ⊢ (𝐶 ⊆ 𝐴 ↔ 𝐶 ⊆ 𝐵)

Syntax hints:   ↔ wb 209   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  sseqtrdi  3978  sseqtri  3986  abss  4017  ssrab  4026  ssindif0  4425  difcom  4450  ssunsn2  4794  ssunpr  4800  sspr  4801  sstp  4802  ssintrab  4937  iunpwss  5074  propssopi  5493  ssimaex  6968  elpwun  7769  ssfi  9158  frfi  9246  alephislim  10068  cardaleph  10074  fin1a2lem12  10396  zornn0g  10490  ssxr  11280  nnwo  12938  isstruct  17213  issubmgm  18761  issubm  18862  grpissubg  19214  issubrng  20633  cntzsubrng  20653  rspvalint  21350  islinds  21940  basdif0  23091  tgdif0  23130  cmpsublem  23537  cmpsub  23538  hauscmplem  23544  2ndcctbss  23593  fbncp  23977  cnextfval  24200  eltsms  24271  reconn  24967  cmssmscld  25490  nobdaymin  27927  nocvxminlem  27928  axcontlem3  29297  axcontlem4  29298  umgredg  29469  nbuhgr  29674  uhgrvd00  29865  vtxdginducedm1  29874  chsscon1i  31795  hatomistici  32695  chirredlem4  32726  atabs2i  32735  mdsymlem1  32736  mdsymlem3  32738  mdsymlem6  32741  mdsymlem8  32743  dmdbr5ati  32755  iundifdif  32888  poimir  38285  ismblfin  38293  cossssid2  39188  ntrk0kbimka  44748  ntrclsk3  44779  ntrneicls11  44799  wfaxrep  45686  wfaxsep  45687  abssf  45813  ssrabf  45815  stoweidlem57  46754  ovnsubadd  47269  ovnovollem3  47355  grlimedgclnbgr  48743  linccl  49177  lincdifsn  49187