Theorem sseq2i 3974

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

Syntax hints:   ↔ wb 209   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  sseqtrdi  3985  sseqtri  3993  abss  4024  ssrab  4033  ssindif0  4427  difcom  4451  ssunsn2  4794  ssunpr  4800  sspr  4801  sstp  4802  ssintrab  4937  iunpwss  5074  propssopi  5489  f1imadifssran  6619  ssimaex  6964  elpwun  7764  ssfi  9153  frfi  9241  alephislim  10063  cardaleph  10069  fin1a2lem12  10391  zornn0g  10485  ssxr  11275  nnwo  12933  isstruct  17208  issubmgm  18756  issubm  18857  grpissubg  19209  issubrng  20628  cntzsubrng  20648  islinds  21924  basdif0  23075  tgdif0  23114  cmpsublem  23521  cmpsub  23522  hauscmplem  23528  2ndcctbss  23577  fbncp  23961  cnextfval  24184  eltsms  24255  reconn  24951  cmssmscld  25474  nobdaymin  27908  nocvxminlem  27909  axcontlem3  29253  axcontlem4  29254  umgredg  29425  nbuhgr  29630  uhgrvd00  29821  vtxdginducedm1  29830  chsscon1i  31751  hatomistici  32651  chirredlem4  32682  atabs2i  32691  mdsymlem1  32692  mdsymlem3  32694  mdsymlem6  32697  mdsymlem8  32699  dmdbr5ati  32711  iundifdif  32844  poimir  38187  ismblfin  38195  cossssid2  39092  ntrk0kbimka  44650  ntrclsk3  44681  ntrneicls11  44701  wfaxrep  45588  wfaxsep  45589  abssf  45715  ssrabf  45717  stoweidlem57  46656  ovnsubadd  47171  ovnovollem3  47257  grlimedgclnbgr  48642  linccl  49072  lincdifsn  49082