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

Syntax hints:   ↔ wb 206   = wceq 1540   ⊆ wss 3903

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 3920

This theorem is referenced by:  sseqtrdi  3976  sseqtri  3984  abss  4015  ssrab  4024  ssindif0  4415  difcom  4440  ssunsn2  4778  ssunpr  4785  sspr  4786  sstp  4787  ssintrab  4921  iunpwss  5056  propssopi  5451  f1imadifssran  6568  ssimaex  6908  elpwun  7705  ssfi  9087  frfi  9174  alephislim  9977  cardaleph  9983  fin1a2lem12  10305  zornn0g  10399  ssxr  11185  nnwo  12814  isstruct  17063  issubmgm  18576  issubm  18677  grpissubg  19025  issubrng  20432  cntzsubrng  20452  islinds  21716  basdif0  22838  tgdif0  22877  cmpsublem  23284  cmpsub  23285  hauscmplem  23291  2ndcctbss  23340  fbncp  23724  cnextfval  23947  eltsms  24018  reconn  24715  cmssmscld  25248  nobdaymin  27687  nocvxminlem  27688  axcontlem3  28911  axcontlem4  28912  umgredg  29083  nbuhgr  29288  uhgrvd00  29480  vtxdginducedm1  29489  chsscon1i  31406  hatomistici  32306  chirredlem4  32337  atabs2i  32346  mdsymlem1  32347  mdsymlem3  32349  mdsymlem6  32352  mdsymlem8  32354  dmdbr5ati  32366  iundifdif  32506  poimir  37633  ismblfin  37641  cossssid2  38445  ntrk0kbimka  44012  ntrclsk3  44043  ntrneicls11  44063  wfaxrep  44968  wfaxsep  44969  abssf  45090  ssrabf  45092  stoweidlem57  46038  ovnsubadd  46553  ovnovollem3  46639  grlimedgclnbgr  47979  linccl  48399  lincdifsn  48409