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

Theorem dfom3 4588
Description: Alias for df-iom 4587. Use it instead of df-iom 4587 for naming consistency with set.mm. (Contributed by NM, 6-Aug-1994.)
Assertion
Ref Expression
dfom3  |-  om  =  |^| { x  |  (
(/)  e.  x  /\  A. y  e.  x  suc  y  e.  x ) }
Distinct variable group:    x, y

Proof of Theorem dfom3
StepHypRef Expression
1 df-iom 4587 1  |-  om  =  |^| { x  |  (
(/)  e.  x  /\  A. y  e.  x  suc  y  e.  x ) }
Colors of variables: wff set class
Syntax hints:    /\ wa 104    = wceq 1353    e. wcel 2148   {cab 2163   A.wral 2455   (/)c0 3422   |^|cint 3842   suc csuc 4362   omcom 4586
This theorem depends on definitions:  df-iom 4587
This theorem is referenced by:  omex  4589  peano1  4590  peano2  4591  peano5  4594  bj-dfom  14334
  Copyright terms: Public domain W3C validator