Metamath Proof Explorer

Theorem nf5

Description: Alternate definition of df-nf . (Contributed by Mario Carneiro, 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen, 11-Sep-2021)

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

Proof

Step Hyp Ref Expression
1 df-nf 
 |-  ( F/ x ph <-> ( E. x ph -> A. x ph ) )
2 nfa1 
 |-  F/ x A. x ph
3 2 19.23 
 |-  ( A. x ( ph -> A. x ph ) <-> ( E. x ph -> A. x ph ) )
4 1 3 bitr4i 
 |-  ( F/ x ph <-> A. x ( ph -> A. x ph ) )