Theorem sseq2i 4025

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

Syntax hints:   ↔ wb 206   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

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

This theorem is referenced by:  sseqtri  4032  sseqtrdi  4046  abss  4073  ssrab  4083  ssindif0  4470  difcom  4495  ssunsn2  4832  ssunpr  4839  sspr  4840  sstp  4841  ssintrab  4976  iunpwss  5112  propssopi  5518  dffun2OLDOLD  6575  ssimaex  6994  elpwun  7788  ssfi  9212  frfi  9319  alephislim  10121  cardaleph  10127  fin1a2lem12  10449  zornn0g  10543  ssxr  11328  nnwo  12953  isstruct  17186  issubmgm  18728  issubm  18829  grpissubg  19177  issubrng  20564  cntzsubrng  20584  islinds  21847  basdif0  22976  tgdif0  23015  cmpsublem  23423  cmpsub  23424  hauscmplem  23430  2ndcctbss  23479  fbncp  23863  cnextfval  24086  eltsms  24157  reconn  24864  cmssmscld  25398  nocvxminlem  27837  nocvxmin  27838  axcontlem3  28996  axcontlem4  28997  umgredg  29170  nbuhgr  29375  uhgrvd00  29567  vtxdginducedm1  29576  chsscon1i  31491  hatomistici  32391  chirredlem4  32422  atabs2i  32431  mdsymlem1  32432  mdsymlem3  32434  mdsymlem6  32437  mdsymlem8  32439  dmdbr5ati  32451  iundifdif  32583  poimir  37640  ismblfin  37648  cossssid2  38450  ntrk0kbimka  44029  ntrclsk3  44060  ntrneicls11  44080  wfaxrep  44950  wfaxsep  44951  abssf  45052  ssrabf  45054  stoweidlem57  46013  ovnsubadd  46528  ovnovollem3  46614  linccl  48260  lincdifsn  48270