Metamath Proof Explorer

Theorem nf6

Description: An alternate definition of df-nf . (Contributed by Mario Carneiro, 24-Sep-2016)

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

Proof

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