Metamath Proof Explorer

Theorem nf3

Description: Alternate definition of nonfreeness. (Contributed by BJ, 16-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 nf2 
 |-  ( F/ x ph <-> ( A. x ph \/ -. E. x ph ) )
2 alnex 
 |-  ( A. x -. ph <-> -. E. x ph )
3 2 orbi2i 
 |-  ( ( A. x ph \/ A. x -. ph ) <-> ( A. x ph \/ -. E. x ph ) )
4 1 3 bitr4i 
 |-  ( F/ x ph <-> ( A. x ph \/ A. x -. ph ) )