Theorem sseq2i 3965

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ⊆ wss 3904

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-ex 1809  df-cleq 2754  df-ss 3921

This theorem is used by:  sseqtrdi  3976  sseqtri  3984  abss  4015  ssrab  4024  ssindif0  4423  difcom  4448  ssunsn2  4792  ssunpr  4798  sspr  4799  sstp  4800  ssintrab  4935  iunpwss  5072  propssopi  5490  ssimaex  6966  elpwun  7766  ssfi  9155  frfi  9243  alephislim  10074  cardaleph  10080  fin1a2lem12  10401  zornn0g  10495  ssxr  11285  nnwo  12943  isstruct  17218  issubmgm  18766  issubm  18867  grpissubg  19219  issubrng  20657  cntzsubrng  20677  rspvalint  21380  islinds  21970  basdif0  23121  tgdif0  23160  cmpsublem  23567  cmpsub  23568  hauscmplem  23574  2ndcctbss  23623  fbncp  24007  cnextfval  24230  eltsms  24301  reconn  24997  cmssmscld  25520  nobdaymin  27957  nocvxminlem  27958  axcontlem3  29327  axcontlem4  29328  umgredg  29499  nbuhgr  29704  uhgrvd00  29895  vtxdginducedm1  29904  chsscon1i  31825  hatomistici  32725  chirredlem4  32756  atabs2i  32765  mdsymlem1  32766  mdsymlem3  32768  mdsymlem6  32771  mdsymlem8  32773  dmdbr5ati  32785  iundifdif  32918  poimir  38332  ismblfin  38340  cossssid2  39235  ntrk0kbimka  44793  ntrclsk3  44824  ntrneicls11  44844  wfaxrep  45731  wfaxsep  45732  abssf  45858  ssrabf  45860  stoweidlem57  46799  ovnsubadd  47314  ovnovollem3  47400  grlimedgclnbgr  48788  linccl  49222  lincdifsn  49232