Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bnj19 Structured version   Visualization version   GIF version

Definition df-bnj19 29809
Description: Define the following predicate: 𝐵 is transitive for 𝐴 and 𝑅. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
df-bnj19 ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵)
Distinct variable groups:   𝑥,𝐵   𝑥,𝐴   𝑥,𝑅

Detailed syntax breakdown of Definition df-bnj19
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cB . . 3 class 𝐵
3 cR . . 3 class 𝑅
41, 2, 3w-bnj19 29808 . 2 wff TrFo(𝐵, 𝐴, 𝑅)
5 vx . . . . . 6 setvar 𝑥
65cv 1473 . . . . 5 class 𝑥
71, 3, 6c-bnj14 29800 . . . 4 class pred(𝑥, 𝐴, 𝑅)
87, 2wss 3539 . . 3 wff pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵
98, 5, 2wral 2895 . 2 wff 𝑥𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵
104, 9wb 194 1 wff ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  bnj978  30066  bnj1118  30099  bnj1125  30107  bnj1137  30110  bnj1408  30151
  Copyright terms: Public domain W3C validator