ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  dford3 Unicode version

Theorem dford3 4327
Description: Alias for df-iord 4326. Use it instead of df-iord 4326 for naming consistency with set.mm. (Contributed by Jim Kingdon, 10-Oct-2018.)
Assertion
Ref Expression
dford3  |-  ( Ord 
A  <->  ( Tr  A  /\  A. x  e.  A  Tr  x ) )
Distinct variable group:    x, A

Proof of Theorem dford3
StepHypRef Expression
1 df-iord 4326 1  |-  ( Ord 
A  <->  ( Tr  A  /\  A. x  e.  A  Tr  x ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104   A.wral 2435   Tr wtr 4062   Ord word 4322
This theorem depends on definitions:  df-iord 4326
This theorem is referenced by:  ordeq  4332  ordtr  4338  trssord  4340  ordelord  4341  ord0  4351  ordon  4445  ordsucim  4459  onintonm  4476  ordom  4566  exmidonfinlem  7128  pw1on  7161  bj-nnord  13533  bj-omord  13535
  Copyright terms: Public domain W3C validator