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

Metamath Proof Explorer

Theorem reuan

Description: Introduction of a conjunct into restricted unique existential quantifier, analogous to euan . (Contributed by Alexander van der Vekens, 2-Jul-2017)

Ref Expression
Hypothesis rmoanim.1 
|- F/ x ph
Assertion reuan 
|- ( E! x e. A ( ph /\ ps ) <-> ( ph /\ E! x e. A ps ) )

Proof

Step Hyp Ref Expression
1 rmoanim.1 
 |-  F/ x ph
2 simpl 
 |-  ( ( ph /\ ps ) -> ph )
3 2 a1i 
 |-  ( x e. A -> ( ( ph /\ ps ) -> ph ) )
4 1 3 rexlimi 
 |-  ( E. x e. A ( ph /\ ps ) -> ph )
5 4 adantr 
 |-  ( ( E. x e. A ( ph /\ ps ) /\ E* x e. A ( ph /\ ps ) ) -> ph )
6 simpr 
 |-  ( ( ph /\ ps ) -> ps )
7 6 reximi 
 |-  ( E. x e. A ( ph /\ ps ) -> E. x e. A ps )
8 7 adantr 
 |-  ( ( E. x e. A ( ph /\ ps ) /\ E* x e. A ( ph /\ ps ) ) -> E. x e. A ps )
9 nfre1 
 |-  F/ x E. x e. A ( ph /\ ps )
10 4 adantr 
 |-  ( ( E. x e. A ( ph /\ ps ) /\ x e. A ) -> ph )
11 10 a1d 
 |-  ( ( E. x e. A ( ph /\ ps ) /\ x e. A ) -> ( ps -> ph ) )
12 11 ancrd 
 |-  ( ( E. x e. A ( ph /\ ps ) /\ x e. A ) -> ( ps -> ( ph /\ ps ) ) )
13 6 12 impbid2 
 |-  ( ( E. x e. A ( ph /\ ps ) /\ x e. A ) -> ( ( ph /\ ps ) <-> ps ) )
14 9 13 rmobida 
 |-  ( E. x e. A ( ph /\ ps ) -> ( E* x e. A ( ph /\ ps ) <-> E* x e. A ps ) )
15 14 biimpa 
 |-  ( ( E. x e. A ( ph /\ ps ) /\ E* x e. A ( ph /\ ps ) ) -> E* x e. A ps )
16 5 8 15 jca32 
 |-  ( ( E. x e. A ( ph /\ ps ) /\ E* x e. A ( ph /\ ps ) ) -> ( ph /\ ( E. x e. A ps /\ E* x e. A ps ) ) )
17 reu5 
 |-  ( E! x e. A ( ph /\ ps ) <-> ( E. x e. A ( ph /\ ps ) /\ E* x e. A ( ph /\ ps ) ) )
18 reu5 
 |-  ( E! x e. A ps <-> ( E. x e. A ps /\ E* x e. A ps ) )
19 18 anbi2i 
 |-  ( ( ph /\ E! x e. A ps ) <-> ( ph /\ ( E. x e. A ps /\ E* x e. A ps ) ) )
20 16 17 19 3imtr4i 
 |-  ( E! x e. A ( ph /\ ps ) -> ( ph /\ E! x e. A ps ) )
21 ibar 
 |-  ( ph -> ( ps <-> ( ph /\ ps ) ) )
22 21 adantr 
 |-  ( ( ph /\ x e. A ) -> ( ps <-> ( ph /\ ps ) ) )
23 1 22 reubida 
 |-  ( ph -> ( E! x e. A ps <-> E! x e. A ( ph /\ ps ) ) )
24 23 biimpa 
 |-  ( ( ph /\ E! x e. A ps ) -> E! x e. A ( ph /\ ps ) )
25 20 24 impbii 
 |-  ( E! x e. A ( ph /\ ps ) <-> ( ph /\ E! x e. A ps ) )