Theorem sseq2i 3960

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

Syntax hints:   ↔ wb 206   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  sseqtrdi  3971  sseqtri  3979  abss  4011  ssrab  4020  ssindif0  4413  difcom  4438  ssunsn2  4780  ssunpr  4787  sspr  4788  sstp  4789  ssintrab  4923  iunpwss  5059  propssopi  5453  f1imadifssran  6575  ssimaex  6916  elpwun  7711  ssfi  9093  frfi  9180  alephislim  9985  cardaleph  9991  fin1a2lem12  10313  zornn0g  10407  ssxr  11193  nnwo  12817  isstruct  17070  issubmgm  18618  issubm  18719  grpissubg  19067  issubrng  20471  cntzsubrng  20491  islinds  21755  basdif0  22888  tgdif0  22927  cmpsublem  23334  cmpsub  23335  hauscmplem  23341  2ndcctbss  23390  fbncp  23774  cnextfval  23997  eltsms  24068  reconn  24764  cmssmscld  25297  nobdaymin  27736  nocvxminlem  27737  axcontlem3  28965  axcontlem4  28966  umgredg  29137  nbuhgr  29342  uhgrvd00  29534  vtxdginducedm1  29543  chsscon1i  31463  hatomistici  32363  chirredlem4  32394  atabs2i  32403  mdsymlem1  32404  mdsymlem3  32406  mdsymlem6  32409  mdsymlem8  32411  dmdbr5ati  32423  iundifdif  32563  poimir  37766  ismblfin  37774  cossssid2  38643  ntrk0kbimka  44196  ntrclsk3  44227  ntrneicls11  44247  wfaxrep  45151  wfaxsep  45152  abssf  45272  ssrabf  45274  stoweidlem57  46217  ovnsubadd  46732  ovnovollem3  46818  grlimedgclnbgr  48157  linccl  48576  lincdifsn  48586