Theorem psseq1 2131

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 2078	. . 3 |- (A = B -> (A (_ C <-> B (_ C))
2		neeq1 1587	. . 3 |- (A = B -> (A =/= C <-> B =/= C))
3	1, 2	anbi12d 627	. 2 |- (A = B -> ((A (_ C /\ A =/= C) <-> (B (_ C /\ B =/= C)))
4		df-pss 2051	. 2 |- (A (. C <-> (A (_ C /\ A =/= C))
5		df-pss 2051	. 2 |- (B (. C <-> (B (_ C /\ B =/= C))
6	3, 4, 5	3bitr4g 554	1 |- (A = B -> (A (. C <-> B (. C))

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

This theorem is referenced by:  psseq1i 2133  psseq1d 2136  ssnpss 2145  psstr 2146  sspsstr 2147  npss0 2305  pssnn 4519  infeq5 4601  zornlem 4775  elnp 5072  ltprord 5114  infxpidmlem10 7512  spansncvt 9538  cvbrt 10147  cvcon3t 10149  cvnbtwnt 10151

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