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

Metamath Proof Explorer

Theorem 19.23v

Description: Version of 19.23 with a disjoint variable condition instead of a nonfreeness hypothesis. (Contributed by NM, 28-Jun-1998) Reduce dependencies on axioms. (Revised by Wolf Lammen, 11-Jan-2020) Remove dependency on ax-6 . (Revised by Rohan Ridenour, 15-Apr-2022)

Ref Expression
Assertion 19.23v 
|- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )

Proof

Step Hyp Ref Expression
1 exim 
 |-  ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )
2 ax5e 
 |-  ( E. x ps -> ps )
3 1 2 syl6 
 |-  ( A. x ( ph -> ps ) -> ( E. x ph -> ps ) )
4 ax-5 
 |-  ( ps -> A. x ps )
5 4 imim2i 
 |-  ( ( E. x ph -> ps ) -> ( E. x ph -> A. x ps ) )
6 19.38 
 |-  ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) )
7 5 6 syl 
 |-  ( ( E. x ph -> ps ) -> A. x ( ph -> ps ) )
8 3 7 impbii 
 |-  ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) )