Theorem psseq1 1559

Description: Equality theorem for proper subclass.

Assertion

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

Proof of Theorem psseq1

Step	Hyp	Ref	Expression
1		sseq1 1521	. . 3 |- (A = B -> (A (_ C <-> B (_ C))
2		neeq1 1194	. . 3 |- (A = B -> (A =/= C <-> B =/= C))
3	1, 2	anbi12d 476	. 2 |- (A = B -> ((A (_ C /\ A =/= C) <-> (B (_ C /\ B =/= C)))
4		df-pss 1494	. 2 |- (A (. C <-> (A (_ C /\ A =/= C))
5		df-pss 1494	. 2 |- (B (. C <-> (B (_ C /\ B =/= C))
6	3, 4, 5	3bitr4g 428	1 |- (A = B -> (A (. C <-> B (. C))

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

This theorem is referenced by:  psseq1i 1561  psseq1d 1564  ssnpss 1573  psstr 1574  sspsstr 1575  npss0 1731  pssnn 3428  inf5 3472  zorn2lem 3610  elnp 3886  ltprord 3928  infxpidmlem10 4942  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