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 ) )