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

Metamath Proof Explorer

Theorem euan

Description: Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 19-Feb-2005) (Proof shortened by Andrew Salmon, 9-Jul-2011) (Proof shortened by Wolf Lammen, 24-Dec-2018)

Ref Expression
Hypothesis moanim.1 
|- F/ x ph
Assertion euan 
|- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )

Proof

Step Hyp Ref Expression
1 moanim.1 
 |-  F/ x ph
2 euex 
 |-  ( E! x ( ph /\ ps ) -> E. x ( ph /\ ps ) )
3 simpl 
 |-  ( ( ph /\ ps ) -> ph )
4 1 3 exlimi 
 |-  ( E. x ( ph /\ ps ) -> ph )
5 2 4 syl 
 |-  ( E! x ( ph /\ ps ) -> ph )
6 ibar 
 |-  ( ph -> ( ps <-> ( ph /\ ps ) ) )
7 1 6 eubid 
 |-  ( ph -> ( E! x ps <-> E! x ( ph /\ ps ) ) )
8 7 biimprcd 
 |-  ( E! x ( ph /\ ps ) -> ( ph -> E! x ps ) )
9 5 8 jcai 
 |-  ( E! x ( ph /\ ps ) -> ( ph /\ E! x ps ) )
10 7 biimpa 
 |-  ( ( ph /\ E! x ps ) -> E! x ( ph /\ ps ) )
11 9 10 impbii 
 |-  ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )