Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Nonfreeness
bj-nnfe
Next ⟩
bj-nnfed
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-nnfe
Description:
Nonfreeness implies the equivalent of
ax5e
.
(Contributed by
BJ
, 28-Jul-2023)
Ref
Expression
Assertion
bj-nnfe
⊢
Ⅎ'
x
φ
→
∃
x
φ
→
φ
Proof
Step
Hyp
Ref
Expression
1
df-bj-nnf
⊢
Ⅎ'
x
φ
↔
∃
x
φ
→
φ
∧
φ
→
∀
x
φ
2
1
simplbi
⊢
Ⅎ'
x
φ
→
∃
x
φ
→
φ