Theorem psseq2 2126

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 2073	. . 3 |- (A = B -> (C (_ A <-> C (_ B))
2		neeq2 1583	. . 3 |- (A = B -> (C =/= A <-> C =/= B))
3	1, 2	anbi12d 626	. 2 |- (A = B -> ((C (_ A /\ C =/= A) <-> (C (_ B /\ C =/= B)))
4		df-pss 2045	. 2 |- (C (. A <-> (C (_ A /\ C =/= A))
5		df-pss 2045	. 2 |- (C (. B <-> (C (_ B /\ C =/= B))
6	3, 4, 5	3bitr4g 553	1 |- (A = B -> (C (. A <-> C (. B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   =/= wne 1577   (_ wss 2037   (. wpss 2038

This theorem is referenced by:  psseq2i 2128  psseq2d 2131  psssstr 2142  php 4493  php2 4494  pssnn 4513  zornlem 4767  elnp 5064  ltprord 5106  infxpidmlem10 7504  infxpidmlem11 7505  spansncvt 9515  cvbrt 10119  cvcon3t 10121  cvnbtwnt 10123  cvbr3 10202

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-ne 1579  df-in 2041  df-ss 2043  df-pss 2045

Copyright terms: Public domain