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 206   = wceq 1540   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  sseqtrdi  3978  sseqtri  3986  abss  4017  ssrab  4026  ssindif0  4417  difcom  4442  ssunsn2  4781  ssunpr  4788  sspr  4789  sstp  4790  ssintrab  4924  iunpwss  5059  propssopi  5455  f1imadifssran  6572  ssimaex  6912  elpwun  7709  ssfi  9097  frfi  9190  alephislim  9996  cardaleph  10002  fin1a2lem12  10324  zornn0g  10418  ssxr  11203  nnwo  12832  isstruct  17081  issubmgm  18594  issubm  18695  grpissubg  19043  issubrng  20450  cntzsubrng  20470  islinds  21734  basdif0  22856  tgdif0  22895  cmpsublem  23302  cmpsub  23303  hauscmplem  23309  2ndcctbss  23358  fbncp  23742  cnextfval  23965  eltsms  24036  reconn  24733  cmssmscld  25266  nobdaymin  27705  nocvxminlem  27706  axcontlem3  28929  axcontlem4  28930  umgredg  29101  nbuhgr  29306  uhgrvd00  29498  vtxdginducedm1  29507  chsscon1i  31424  hatomistici  32324  chirredlem4  32355  atabs2i  32364  mdsymlem1  32365  mdsymlem3  32367  mdsymlem6  32370  mdsymlem8  32372  dmdbr5ati  32384  iundifdif  32524  poimir  37635  ismblfin  37643  cossssid2  38447  ntrk0kbimka  44015  ntrclsk3  44046  ntrneicls11  44066  wfaxrep  44971  wfaxsep  44972  abssf  45093  ssrabf  45095  stoweidlem57  46042  ovnsubadd  46557  ovnovollem3  46643  grlimedgclnbgr  47983  linccl  48403  lincdifsn  48413