Theorem sseq2i 3979

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

Syntax hints:   ↔ wb 206   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  sseqtrdi  3990  sseqtri  3998  abss  4029  ssrab  4039  ssindif0  4430  difcom  4455  ssunsn2  4794  ssunpr  4801  sspr  4802  sstp  4803  ssintrab  4938  iunpwss  5074  propssopi  5471  dffun2OLDOLD  6526  f1imadifssran  6605  ssimaex  6949  elpwun  7748  ssfi  9143  frfi  9239  alephislim  10043  cardaleph  10049  fin1a2lem12  10371  zornn0g  10465  ssxr  11250  nnwo  12879  isstruct  17129  issubmgm  18636  issubm  18737  grpissubg  19085  issubrng  20463  cntzsubrng  20483  islinds  21725  basdif0  22847  tgdif0  22886  cmpsublem  23293  cmpsub  23294  hauscmplem  23300  2ndcctbss  23349  fbncp  23733  cnextfval  23956  eltsms  24027  reconn  24724  cmssmscld  25257  nocvxminlem  27696  nocvxmin  27697  axcontlem3  28900  axcontlem4  28901  umgredg  29072  nbuhgr  29277  uhgrvd00  29469  vtxdginducedm1  29478  chsscon1i  31398  hatomistici  32298  chirredlem4  32329  atabs2i  32338  mdsymlem1  32339  mdsymlem3  32341  mdsymlem6  32344  mdsymlem8  32346  dmdbr5ati  32358  iundifdif  32498  poimir  37654  ismblfin  37662  cossssid2  38466  ntrk0kbimka  44035  ntrclsk3  44066  ntrneicls11  44086  wfaxrep  44991  wfaxsep  44992  abssf  45113  ssrabf  45115  stoweidlem57  46062  ovnsubadd  46577  ovnovollem3  46663  linccl  48407  lincdifsn  48417