This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 19.9t

Description: Closed form of 19.9 and version of 19.3t with an existential quantifier. (Contributed by NM, 13-May-1993) (Revised by Mario Carneiro, 24-Sep-2016) (Proof shortened by Wolf Lammen, 14-Jul-2020)

Ref Expression
Assertion 19.9t 
|- ( F/ x ph -> ( E. x ph <-> ph ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( F/ x ph -> F/ x ph )
2 1 19.9d 
 |-  ( F/ x ph -> ( E. x ph -> ph ) )
3 19.8a 
 |-  ( ph -> E. x ph )
4 2 3 impbid1 
 |-  ( F/ x ph -> ( E. x ph <-> ph ) )