Theorem psseq2 2698

Description: Equality theorem for proper subclass.

Assertion

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

Proof of Theorem psseq2

Step	Hyp	Ref	Expression
1		sseq2 2639	. . 3 |- (A = B -> (C C_ A <-> C C_ B))
2		neeq2 2025	. . 3 |- (A = B -> (C =/= A <-> C =/= B))
3	1, 2	anbi12d 690	. 2 |- (A = B -> ((C C_ A /\ C =/= A) <-> (C C_ B /\ C =/= B)))
4		df-pss 2607	. 2 |- (C C. A <-> (C C_ A /\ C =/= A))
5		df-pss 2607	. 2 |- (C C. B <-> (C C_ B /\ C =/= B))
6	3, 4, 5	3bitr4g 614	1 |- (A = B -> (C C. A <-> C C. B))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   = wceq 1298   =/= wne 2017   C_ wss 2593   C. wpss 2594

This theorem is referenced by:  psseq2i 2700  psseq2d 2703  psssstr 2716  php 5607  php2 5608  pssnn 5628  zornlem 5957  elnp 6244  ltprord 6286  infxpidmlem10 8830  infxpidmlem11 8831  spansncv 11233  cvbr 11854  cvcon3 11856  cvnbtwn 11858  cvbr3i 11939  dfon2lem6 13854  dfon2lem7 13855  dfon2lem8 13856  dfon2 13858  alexsublem4 15440  filssufil 15571

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-10 1308  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-in 2603  df-ss 2605  df-pss 2607

Copyright terms: Public domain