Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-rnf Structured version   Visualization version   GIF version

Definition df-bj-rnf 32123
Description: Definition of restricted non-freeness. Informally, the proposition 𝑥𝐴𝜑 means that 𝜑(𝑥) does not vary on 𝐴. (Contributed by BJ, 19-Mar-2021.)
Assertion
Ref Expression
df-bj-rnf (Ⅎ𝑥𝐴𝜑 ↔ (∃𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜑))

Detailed syntax breakdown of Definition df-bj-rnf
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
3 cA . . 3 class 𝐴
41, 2, 3wrnf 32122 . 2 wff 𝑥𝐴𝜑
51, 2, 3wrex 2897 . . 3 wff 𝑥𝐴 𝜑
61, 2, 3wral 2896 . . 3 wff 𝑥𝐴 𝜑
75, 6wi 4 . 2 wff (∃𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜑)
84, 7wb 195 1 wff (Ⅎ𝑥𝐴𝜑 ↔ (∃𝑥𝐴 𝜑 → ∀𝑥𝐴 𝜑))
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator