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

Metamath Proof Explorer

Theorem euanv

Description: Introduction of a conjunct into unique existential quantifier. (Contributed by NM, 23-Mar-1995) Reduce dependencies on axioms. (Revised by Wolf Lammen, 14-Jan-2023)

Ref Expression
Assertion euanv 
|- ( E! x ( ph /\ ps ) <-> ( ph /\ E! x ps ) )

Proof

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