Theorem sseq2i 4013

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

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

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 2708

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

This theorem is referenced by:  sseqtrdi  4024  sseqtri  4032  abss  4063  ssrab  4073  ssindif0  4464  difcom  4489  ssunsn2  4827  ssunpr  4834  sspr  4835  sstp  4836  ssintrab  4971  iunpwss  5107  propssopi  5513  dffun2OLDOLD  6573  f1imadifssran  6652  ssimaex  6994  elpwun  7789  ssfi  9213  frfi  9321  alephislim  10123  cardaleph  10129  fin1a2lem12  10451  zornn0g  10545  ssxr  11330  nnwo  12955  isstruct  17189  issubmgm  18715  issubm  18816  grpissubg  19164  issubrng  20547  cntzsubrng  20567  islinds  21829  basdif0  22960  tgdif0  22999  cmpsublem  23407  cmpsub  23408  hauscmplem  23414  2ndcctbss  23463  fbncp  23847  cnextfval  24070  eltsms  24141  reconn  24850  cmssmscld  25384  nocvxminlem  27822  nocvxmin  27823  axcontlem3  28981  axcontlem4  28982  umgredg  29155  nbuhgr  29360  uhgrvd00  29552  vtxdginducedm1  29561  chsscon1i  31481  hatomistici  32381  chirredlem4  32412  atabs2i  32421  mdsymlem1  32422  mdsymlem3  32424  mdsymlem6  32427  mdsymlem8  32429  dmdbr5ati  32441  iundifdif  32575  poimir  37660  ismblfin  37668  cossssid2  38469  ntrk0kbimka  44052  ntrclsk3  44083  ntrneicls11  44103  wfaxrep  45011  wfaxsep  45012  abssf  45117  ssrabf  45119  stoweidlem57  46072  ovnsubadd  46587  ovnovollem3  46673  linccl  48331  lincdifsn  48341