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 208   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  sseqtrdi  3974  sseqtri  3982  abss  4013  ssrab  4022  ssindif0  4415  difcom  4439  ssunsn2  4782  ssunpr  4789  sspr  4790  sstp  4791  ssintrab  4926  iunpwss  5061  propssopi  5474  f1imadifssran  6602  ssimaex  6947  elpwun  7747  ssfi  9135  frfi  9223  alephislim  10033  cardaleph  10039  fin1a2lem12  10362  zornn0g  10456  ssxr  11246  nnwo  12908  isstruct  17179  issubmgm  18727  issubm  18828  grpissubg  19179  issubrng  20584  cntzsubrng  20604  islinds  21849  basdif0  23001  tgdif0  23040  cmpsublem  23447  cmpsub  23448  hauscmplem  23454  2ndcctbss  23503  fbncp  23887  cnextfval  24110  eltsms  24181  reconn  24877  cmssmscld  25400  nobdaymin  27834  nocvxminlem  27835  axcontlem3  29124  axcontlem4  29125  umgredg  29296  nbuhgr  29501  uhgrvd00  29692  vtxdginducedm1  29701  chsscon1i  31622  hatomistici  32522  chirredlem4  32553  atabs2i  32562  mdsymlem1  32563  mdsymlem3  32565  mdsymlem6  32568  mdsymlem8  32570  dmdbr5ati  32582  iundifdif  32722  poimir  38113  ismblfin  38121  cossssid2  39018  ntrk0kbimka  44576  ntrclsk3  44607  ntrneicls11  44627  wfaxrep  45531  wfaxsep  45532  abssf  45651  ssrabf  45653  stoweidlem57  46592  ovnsubadd  47107  ovnovollem3  47193  grlimedgclnbgr  48578  linccl  48997  lincdifsn  49007