Theorem relss 3241

Description: Subclass theorem for relation predicate. Theorem 2 of [Suppes] p. 58.

Assertion

Ref	Expression
relss	|- (A (_ B -> (Rel B -> Rel A))

Proof of Theorem relss

Step	Hyp	Ref	Expression
1		sstr2 2067	. 2 |- (A (_ B -> (B (_ (V X. V) -> A (_ (V X. V)))
2		df-rel 3180	. 2 |- (Rel B <-> B (_ (V X. V))
3		df-rel 3180	. 2 |- (Rel A <-> A (_ (V X. V))
4	1, 2, 3	3imtr4g 552	1 |- (A (_ B -> (Rel B -> Rel A))

Syntax hints:   -> wi 3  Vcvv 1807   (_ wss 2043   X. cxp 3163  Rel wrel 3170

This theorem is referenced by:  relin1 3257  relin2 3258  reldif 3259  iss 3389  intasym 3430  asymref 3431  intirr 3433  funss 3526  funssres 3544  prcdpq 5077  phrel 8418  bnrel 8471  hlrel 8538

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-in 2047  df-ss 2049  df-rel 3180

Copyright terms: Public domain