Theorem sseq2i 3960

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

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

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 2155  ax-ext 2733

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

This theorem is used by:  sseqtrdi  3971  sseqtri  3979  abss  4010  ssrab  4019  ssindif0  4417  difcom  4444  ssunsn2  4788  ssunpr  4794  sspr  4795  sstp  4796  ssintrab  4931  iunpwss  5067  propssopi  5480  imadifssrn  6200  ssimaex  6968  elpwun  7781  ssfi  9181  frfi  9269  alephislim  10155  cardaleph  10161  fin1a2lem12  10482  zornn0g  10576  ssxr  11372  nnwo  13033  isstruct  17323  issubmgm  18884  issubm  18991  grpissubg  19350  issubrng  20792  cntzsubrng  20812  rspvalint  21516  islinds  22108  basdif0  23264  tgdif0  23303  cmpsublem  23710  cmpsub  23711  hauscmplem  23717  2ndcctbss  23767  fbncp  24151  cnextfval  24374  eltsms  24445  reconn  25141  cmssmscld  25664  nobdaymin  28132  nocvxminlem  28133  axcontlem3  29537  axcontlem4  29538  umgredg  29709  nbuhgr  29917  uhgrvd00  30108  vtxdginducedm1  30117  chsscon1i  32057  hatomistici  32957  chirredlem4  32988  atabs2i  32997  mdsymlem1  32998  mdsymlem3  33000  mdsymlem6  33003  mdsymlem8  33005  dmdbr5ati  33017  iundifdif  33150  poimir  38551  ismblfin  38559  cossssid2  39470  ntrk0kbimka  45024  ntrclsk3  45055  ntrneicls11  45075  wfaxrep  45962  wfaxsep  45963  abssf  46096  ssrabf  46098  stoweidlem57  47036  ovnsubadd  47551  ovnovollem3  47637  grlimedgclnbgr  49062  linccl  49495  lincdifsn  49505