Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for BJ
First-order logic
Nonfreeness
bj-nnfe1
Next ⟩
bj-19.12
Metamath Proof Explorer
Ascii
Unicode
Theorem
bj-nnfe1
Description:
See
nfe1
.
(Contributed by
BJ
, 12-Aug-2023)
(Proof modification is discouraged.)
Ref
Expression
Assertion
bj-nnfe1
⊢
Ⅎ'
x
∃
x
φ
Proof
Step
Hyp
Ref
Expression
1
bj-modal4e
⊢
∃
x
∃
x
φ
→
∃
x
φ
2
hbe1
⊢
∃
x
φ
→
∀
x
∃
x
φ
3
df-bj-nnf
⊢
Ⅎ'
x
∃
x
φ
↔
∃
x
∃
x
φ
→
∃
x
φ
∧
∃
x
φ
→
∀
x
∃
x
φ
4
1
2
3
mpbir2an
⊢
Ⅎ'
x
∃
x
φ