Metamath Proof Explorer

Theorem bj-eximALT

Description: Alternate proof of exim directly from alim by using df-ex (using duality of A. and E. . (Contributed by BJ, 9-Dec-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-eximALT 
|- ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )

Proof

Step Hyp Ref Expression
1 con3 
 |-  ( ( ph -> ps ) -> ( -. ps -> -. ph ) )
2 1 alimi 
 |-  ( A. x ( ph -> ps ) -> A. x ( -. ps -> -. ph ) )
3 alim 
 |-  ( A. x ( -. ps -> -. ph ) -> ( A. x -. ps -> A. x -. ph ) )
4 con3 
 |-  ( ( A. x -. ps -> A. x -. ph ) -> ( -. A. x -. ph -> -. A. x -. ps ) )
5 2 3 4 3syl 
 |-  ( A. x ( ph -> ps ) -> ( -. A. x -. ph -> -. A. x -. ps ) )
6 df-ex 
 |-  ( E. x ph <-> -. A. x -. ph )
7 df-ex 
 |-  ( E. x ps <-> -. A. x -. ps )
8 5 6 7 3imtr4g 
 |-  ( A. x ( ph -> ps ) -> ( E. x ph -> E. x ps ) )