Theorem sseq2i 3528

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 3525	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  <->wb 184  =wceq 1395  C_wss 3475

This theorem is referenced by:  sseqtri  3535  syl6sseq  3549  abss  3568  ssrab  3577  ssindif0  3880  difcom  3912  ssunsn2  4189  ssunpr  4192  sspr  4193  sstp  4194  ssintrab  4310  iunpwss  4420  dffun2  5603  ssimaex  5938  elpwun  6613  frfi  7785  alephislim  8485  cardaleph  8491  fin1a2lem12  8812  zornn0g  8906  ssxr  9675  nnwo  11176  isstruct  14642  issubm  15978  grpissubg  16221  islinds  18844  basdif0  19454  tgdif0  19494  cmpsublem  19899  cmpsub  19900  hauscmplem  19906  2ndcctbss  19956  fbncp  20340  cnextfval  20562  eltsms  20631  reconn  21333  axcontlem3  24269  axcontlem4  24270  chsscon1i  26380  hatomistici  27281  chirredlem4  27312  atabs2i  27321  mdsymlem1  27322  mdsymlem3  27324  mdsymlem6  27327  mdsymlem8  27329  dmdbr5ati  27341  iundifdif  27430  nocvxminlem  29450  nocvxmin  29451  ismblfin  30055  stoweidlem57  31839  issubmgm  32477  linccl  33015  lincdifsn  33025

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489