Theorem sseq2i 3988

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

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

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  sseqtrdi  3999  sseqtri  4007  abss  4038  ssrab  4048  ssindif0  4439  difcom  4464  ssunsn2  4803  ssunpr  4810  sspr  4811  sstp  4812  ssintrab  4947  iunpwss  5083  propssopi  5483  dffun2OLDOLD  6543  f1imadifssran  6622  ssimaex  6964  elpwun  7763  ssfi  9187  frfi  9293  alephislim  10097  cardaleph  10103  fin1a2lem12  10425  zornn0g  10519  ssxr  11304  nnwo  12929  isstruct  17171  issubmgm  18680  issubm  18781  grpissubg  19129  issubrng  20507  cntzsubrng  20527  islinds  21769  basdif0  22891  tgdif0  22930  cmpsublem  23337  cmpsub  23338  hauscmplem  23344  2ndcctbss  23393  fbncp  23777  cnextfval  24000  eltsms  24071  reconn  24768  cmssmscld  25302  nocvxminlem  27741  nocvxmin  27742  axcontlem3  28945  axcontlem4  28946  umgredg  29117  nbuhgr  29322  uhgrvd00  29514  vtxdginducedm1  29523  chsscon1i  31443  hatomistici  32343  chirredlem4  32374  atabs2i  32383  mdsymlem1  32384  mdsymlem3  32386  mdsymlem6  32389  mdsymlem8  32391  dmdbr5ati  32403  iundifdif  32543  poimir  37677  ismblfin  37685  cossssid2  38486  ntrk0kbimka  44063  ntrclsk3  44094  ntrneicls11  44114  wfaxrep  45019  wfaxsep  45020  abssf  45136  ssrabf  45138  stoweidlem57  46086  ovnsubadd  46601  ovnovollem3  46687  linccl  48390  lincdifsn  48400