Theorem sseq2i 3630

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

Syntax hints:   ↔ wb 196   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sseqtri  3637  syl6sseq  3651  abss  3671  ssrab  3680  ssindif0  4031  difcom  4053  ssunsn2  4359  ssunpr  4365  sspr  4366  sstp  4367  ssintrab  4500  iunpwss  4618  propssopi  4971  dffun2  5898  ssimaex  6263  elpwun  6977  frfi  8205  alephislim  8906  cardaleph  8912  fin1a2lem12  9233  zornn0g  9327  ssxr  10107  nnwo  11753  isstruct  15870  issubm  17347  grpissubg  17614  islinds  20148  basdif0  20757  tgdif0  20796  cmpsublem  21202  cmpsub  21203  hauscmplem  21209  2ndcctbss  21258  fbncp  21643  cnextfval  21866  eltsms  21936  reconn  22631  axcontlem3  25846  axcontlem4  25847  umgredg  26033  nbuhgr  26239  uhgrvd00  26430  vtxdginducedm1  26439  chsscon1i  28321  hatomistici  29221  chirredlem4  29252  atabs2i  29261  mdsymlem1  29262  mdsymlem3  29264  mdsymlem6  29267  mdsymlem8  29269  dmdbr5ati  29281  iundifdif  29381  nocvxminlem  31893  nocvxmin  31894  poimir  33442  ismblfin  33450  ntrk0kbimka  38337  ntrclsk3  38368  ntrneicls11  38388  abssf  39295  ssrabf  39298  stoweidlem57  40274  ovnsubadd  40786  ovnovollem3  40872  issubmgm  41789  linccl  42203  lincdifsn  42213