Theorem sseq2i 4038

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  sseqtri  4045  sseqtrdi  4059  abss  4086  ssrab  4096  ssindif0  4487  difcom  4512  ssunsn2  4852  ssunpr  4859  sspr  4860  sstp  4861  ssintrab  4995  iunpwss  5130  propssopi  5527  dffun2OLDOLD  6585  ssimaex  7007  elpwun  7804  ssfi  9240  frfi  9349  alephislim  10152  cardaleph  10158  fin1a2lem12  10480  zornn0g  10574  ssxr  11359  nnwo  12978  isstruct  17199  issubmgm  18740  issubm  18838  grpissubg  19186  issubrng  20573  cntzsubrng  20593  islinds  21852  basdif0  22981  tgdif0  23020  cmpsublem  23428  cmpsub  23429  hauscmplem  23435  2ndcctbss  23484  fbncp  23868  cnextfval  24091  eltsms  24162  reconn  24869  cmssmscld  25403  nocvxminlem  27840  nocvxmin  27841  axcontlem3  28999  axcontlem4  29000  umgredg  29173  nbuhgr  29378  uhgrvd00  29570  vtxdginducedm1  29579  chsscon1i  31494  hatomistici  32394  chirredlem4  32425  atabs2i  32434  mdsymlem1  32435  mdsymlem3  32437  mdsymlem6  32440  mdsymlem8  32442  dmdbr5ati  32454  iundifdif  32585  poimir  37613  ismblfin  37621  cossssid2  38424  ntrk0kbimka  44001  ntrclsk3  44032  ntrneicls11  44052  abssf  45014  ssrabf  45016  stoweidlem57  45978  ovnsubadd  46493  ovnovollem3  46579  linccl  48143  lincdifsn  48153