Theorem sseq2i 3959

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  sseqtrdi  3970  sseqtri  3978  abss  4009  ssrab  4018  ssindif0  4409  difcom  4434  ssunsn2  4774  ssunpr  4781  sspr  4782  sstp  4783  ssintrab  4916  iunpwss  5050  propssopi  5443  f1imadifssran  6562  ssimaex  6902  elpwun  7697  ssfi  9077  frfi  9164  alephislim  9969  cardaleph  9975  fin1a2lem12  10297  zornn0g  10391  ssxr  11177  nnwo  12806  isstruct  17058  issubmgm  18605  issubm  18706  grpissubg  19054  issubrng  20457  cntzsubrng  20477  islinds  21741  basdif0  22863  tgdif0  22902  cmpsublem  23309  cmpsub  23310  hauscmplem  23316  2ndcctbss  23365  fbncp  23749  cnextfval  23972  eltsms  24043  reconn  24739  cmssmscld  25272  nobdaymin  27711  nocvxminlem  27712  axcontlem3  28939  axcontlem4  28940  umgredg  29111  nbuhgr  29316  uhgrvd00  29508  vtxdginducedm1  29517  chsscon1i  31434  hatomistici  32334  chirredlem4  32365  atabs2i  32374  mdsymlem1  32375  mdsymlem3  32377  mdsymlem6  32380  mdsymlem8  32382  dmdbr5ati  32394  iundifdif  32534  poimir  37693  ismblfin  37701  cossssid2  38505  ntrk0kbimka  44072  ntrclsk3  44103  ntrneicls11  44123  wfaxrep  45027  wfaxsep  45028  abssf  45149  ssrabf  45151  stoweidlem57  46095  ovnsubadd  46610  ovnovollem3  46696  grlimedgclnbgr  48026  linccl  48446  lincdifsn  48456