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 31955
 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 31954 . 2 wff TrFo(𝐵, 𝐴, 𝑅)
5 vx . . . . . 6 setvar 𝑥
65cv 1529 . . . . 5 class 𝑥
71, 3, 6c-bnj14 31946 . . . 4 class pred(𝑥, 𝐴, 𝑅)
87, 2wss 3934 . . 3 wff pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵
98, 5, 2wral 3136 . 2 wff 𝑥𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵
104, 9wb 208 1 wff ( TrFo(𝐵, 𝐴, 𝑅) ↔ ∀𝑥𝐵 pred(𝑥, 𝐴, 𝑅) ⊆ 𝐵)
 Colors of variables: wff setvar class This definition is referenced by:  bnj978  32209  bnj1118  32244  bnj1125  32252  bnj1137  32255  bnj1408  32296
 Copyright terms: Public domain W3C validator