Theorem psseq2 3591

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

Assertion

Ref	Expression
psseq2

Proof of Theorem psseq2

Step	Hyp	Ref	Expression
1		sseq2 3525	. . 3
2		neeq2 2740	. . 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:  psseq2i  3593  psseq2d  3596  psssstr  3609  brrpssg  6582  sorpssint  6590  php  7721  php2  7722  pssnn  7758  isfin4  8698  fin2i2  8719  elnp  9386  elnpi  9387  ltprord  9429  pgpfac1lem1  17125  pgpfac1lem5  17130  lbsextlem4  17807  alexsubALTlem4  20550  spansncv  26571  cvbr  27201  cvcon3  27203  cvnbtwn  27205  cvbr4i  27286  dfon2lem6  29220  dfon2lem7  29221  dfon2lem8  29222  dfon2  29224  lcvbr  34746  lcvnbtwn  34750  lsatcv0  34756  lsat0cv  34758  islshpcv  34778  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