Theorem sseq2i 3952

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

Syntax hints:   ↔ wb 206   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  sseqtrdi  3963  sseqtri  3971  abss  4003  ssrab  4012  ssindif0  4405  difcom  4429  ssunsn2  4771  ssunpr  4778  sspr  4779  sstp  4780  ssintrab  4914  iunpwss  5050  propssopi  5456  f1imadifssran  6578  ssimaex  6919  elpwun  7716  ssfi  9100  frfi  9188  alephislim  9996  cardaleph  10002  fin1a2lem12  10324  zornn0g  10418  ssxr  11206  nnwo  12854  isstruct  17113  issubmgm  18661  issubm  18762  grpissubg  19113  issubrng  20515  cntzsubrng  20535  islinds  21799  basdif0  22928  tgdif0  22967  cmpsublem  23374  cmpsub  23375  hauscmplem  23381  2ndcctbss  23430  fbncp  23814  cnextfval  24037  eltsms  24108  reconn  24804  cmssmscld  25327  nobdaymin  27759  nocvxminlem  27760  axcontlem3  29049  axcontlem4  29050  umgredg  29221  nbuhgr  29426  uhgrvd00  29618  vtxdginducedm1  29627  chsscon1i  31548  hatomistici  32448  chirredlem4  32479  atabs2i  32488  mdsymlem1  32489  mdsymlem3  32491  mdsymlem6  32494  mdsymlem8  32496  dmdbr5ati  32508  iundifdif  32647  poimir  37988  ismblfin  37996  cossssid2  38893  ntrk0kbimka  44484  ntrclsk3  44515  ntrneicls11  44535  wfaxrep  45439  wfaxsep  45440  abssf  45560  ssrabf  45562  stoweidlem57  46503  ovnsubadd  47018  ovnovollem3  47104  grlimedgclnbgr  48483  linccl  48902  lincdifsn  48912