Theorem psseq2 2132

Description: Equality theorem for proper subclass.

Assertion

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

Proof of Theorem psseq2

Step	Hyp	Ref	Expression
1		sseq2 2079	. . 3 |- (A = B -> (C (_ A <-> C (_ B))
2		neeq2 1588	. . 3 |- (A = B -> (C =/= A <-> C =/= B))
3	1, 2	anbi12d 627	. 2 |- (A = B -> ((C (_ A /\ C =/= A) <-> (C (_ B /\ C =/= B)))
4		df-pss 2051	. 2 |- (C (. A <-> (C (_ A /\ C =/= A))
5		df-pss 2051	. 2 |- (C (. B <-> (C (_ B /\ C =/= B))
6	3, 4, 5	3bitr4g 554	1 |- (A = B -> (C (. A <-> C (. B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 954   =/= wne 1582   (_ wss 2043   (. wpss 2044

This theorem is referenced by:  psseq2i 2134  psseq2d 2137  psssstr 2148  php 4499  php2 4500  pssnn 4519  zornlem 4775  elnp 5072  ltprord 5114  infxpidmlem10 7512  infxpidmlem11 7513  spansncvt 9538  cvbrt 10147  cvcon3t 10149  cvnbtwnt 10151  cvbr3 10231

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-in 2047  df-ss 2049  df-pss 2051

Copyright terms: Public domain