Metamath Proof Explorer

Theorem xfree

Description: A partial converse to 19.9t . (Contributed by Stefan Allan, 21-Dec-2008) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Assertion xfree 
|- ( A. x ( ph -> A. x ph ) <-> A. x ( E. x ph -> ph ) )

Proof

Step Hyp Ref Expression
1 nf5 
 |-  ( F/ x ph <-> A. x ( ph -> A. x ph ) )
2 nf6 
 |-  ( F/ x ph <-> A. x ( E. x ph -> ph ) )
3 1 2 bitr3i 
 |-  ( A. x ( ph -> A. x ph ) <-> A. x ( E. x ph -> ph ) )