Metamath Proof Explorer

Theorem nf4

Description: Alternate definition of non-freeness. This definition uses only primitive symbols ( -> , -. , A. ). (Contributed by BJ, 16-Sep-2021)

Ref Expression
Assertion nf4 
|- ( F/ x ph <-> ( -. A. x ph -> A. x -. ph ) )

Proof

Step Hyp Ref Expression
1 nf3 
 |-  ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) )
2 df-or 
 |-  ( ( A. x ph \/ A. x -. ph ) <-> ( -. A. x ph -> A. x -. ph ) )
3 1 2 bitri 
 |-  ( F/ x ph <-> ( -. A. x ph -> A. x -. ph ) )