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 32246
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 32245 . 2 wff TrFo(𝐵, 𝐴, 𝑅)
5 vx . . . . . 6 setvar 𝑥
65cv 1541 . . . . 5 class 𝑥
71, 3, 6c-bnj14 32237 . . . 4 class pred(𝑥, 𝐴, 𝑅)
87, 2wss 3843 . . 3 wff pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵
98, 5, 2wral 3053 . 2 wff 𝑥𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵
104, 9wb 209 1 wff ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵)
Colors of variables: wff setvar class
This definition is referenced by:  bnj978  32500  bnj1118  32535  bnj1125  32543  bnj1137  32546  bnj1408  32587
  Copyright terms: Public domain W3C validator