Theorem psseq2 1560

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 1522	. . 3 |- (A = B -> (C (_ A <-> C (_ B))
2		neeq2 1195	. . 3 |- (A = B -> (C =/= A <-> C =/= B))
3	1, 2	anbi12d 476	. 2 |- (A = B -> ((C (_ A /\ C =/= A) <-> (C (_ B /\ C =/= B)))
4		df-pss 1494	. 2 |- (C (. A <-> (C (_ A /\ C =/= A))
5		df-pss 1494	. 2 |- (C (. B <-> (C (_ B /\ C =/= B))
6	3, 4, 5	3bitr4g 428	1 |- (A = B -> (C (. A <-> C (. B))

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196   = wceq 1091   =/= wne 1190   (_ wss 1487   (. wpss 1488

This theorem is referenced by:  psseq2i 1562  psseq2d 1565  psssstr 1576  php 3409  php2 3410  pssnn 3428  zorn2lem 3610  elnp 3886  ltprord 3928  infxpidmlem10 4942  infxpidmlem11 4943  spansncvt 5543  cvbrt 5714  cvcon3t 5716  cvnbtwnt 5718

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-in 1491  df-ss 1492  df-pss 1494

metamath.org