Theorem psseq2 3695

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

Assertion

Ref	Expression
psseq2	|- ( A = B -> ( C C. A <-> C C. B ) )

Proof of Theorem psseq2

Step	Hyp	Ref	Expression
1		sseq2 3627	. . 3 |- ( A = B -> ( C C_ A <-> C C_ B ) )
2		neeq2 2857	. . 3 |- ( A = B -> ( C =/= A <-> C =/= B ) )
3	1, 2	anbi12d 747	. 2 |- ( A = B -> ( ( C C_ A /\ C =/= A ) <-> ( C C_ B /\ C =/= B ) ) )
4		df-pss 3590	. 2 |- ( C C. A <-> ( C C_ A /\ C =/= A ) )
5		df-pss 3590	. 2 |- ( C C. B <-> ( C C_ B /\ C =/= B ) )
6	3, 4, 5	3bitr4g 303	1 |- ( A = B -> ( C C. A <-> C C. B ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   =/= wne 2794   C_ wss 3574   C. wpss 3575

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-ne 2795  df-in 3581  df-ss 3588  df-pss 3590

This theorem is referenced by:  psseq2i  3697  psseq2d  3700  psssstr  3713  brrpssg  6939  sorpssint  6947  php  8144  php2  8145  pssnn  8178  isfin4  9119  fin2i2  9140  elnp  9809  elnpi  9810  ltprord  9852  pgpfac1lem1  18473  pgpfac1lem5  18478  lbsextlem4  19161  alexsubALTlem4  21854  spansncv  28512  cvbr  29141  cvcon3  29143  cvnbtwn  29145  cvbr4i  29226  dfon2lem6  31693  dfon2lem7  31694  dfon2lem8  31695  dfon2  31697  lcvbr  34308  lcvnbtwn  34312  lsatcv0  34318  lsat0cv  34320  islshpcv  34340  mapdcv  36949