Theorem psseq1 3590

Description: Equality theorem for proper subclass. (Contributed by NM, 7-Feb-1996.)

Assertion

Ref	Expression
psseq1

Proof of Theorem psseq1

Step	Hyp	Ref	Expression
1		sseq1 3524	. . 3
2		neeq1 2738	. . 3
3	1, 2	anbi12d 710	. 2
4		df-pss 3491	. 2
5		df-pss 3491	. 2
6	3, 4, 5	3bitr4g 288	1

Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  =/=wne 2652  C_wss 3475  C.wpss 3476

This theorem is referenced by:  psseq1i  3592  psseq1d  3595  psstr  3607  sspsstr  3608  brrpssg  6582  sorpssuni  6589  pssnn  7758  marypha1lem  7913  infeq5i  8074  infpss  8618  fin4i  8699  isfin2-2  8720  zornn0g  8906  ttukeylem7  8916  elnp  9386  elnpi  9387  ltprord  9429  pgpfac1lem1  17125  pgpfac1lem5  17130  pgpfac1  17131  pgpfaclem2  17133  pgpfac  17135  islbs3  17801  alexsubALTlem4  20550  wilthlem2  23343  spansncv  26571  cvbr  27201  cvcon3  27203  cvnbtwn  27205  dfon2lem3  29217  dfon2lem4  29218  dfon2lem5  29219  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon2  29224  lcvbr  34746  lcvnbtwn  34750  mapdcv  37387

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-ne 2654  df-in 3482  df-ss 3489  df-pss 3491