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	⊢ Ⅎ 𝑥 𝜑
Assertion	reuan	⊢ ( ∃! 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		rmoanim.1	⊢ Ⅎ 𝑥 𝜑
2		simpl	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜑 )
3	2	a1i	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝜑 ∧ 𝜓 ) → 𝜑 ) )
4	1 3	rexlimi	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → 𝜑 )
5	4	adantr	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ) → 𝜑 )
6		simpr	⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝜓 )
7	6	reximi	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → ∃ 𝑥 ∈ 𝐴 𝜓 )
8	7	adantr	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ) → ∃ 𝑥 ∈ 𝐴 𝜓 )
9		nfre1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 )
10	4	adantr	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → 𝜑 )
11	10	a1d	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝜑 ) )
12	11	ancrd	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) )
13	6 12	impbid2	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝜑 ∧ 𝜓 ) ↔ 𝜓 ) )
14	9 13	rmobida	⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → ( ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ∃* 𝑥 ∈ 𝐴 𝜓 ) )
15	14	biimpa	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ) → ∃* 𝑥 ∈ 𝐴 𝜓 )
16	5 8 15	jca32	⊢ ( ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ) → ( 𝜑 ∧ ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∃* 𝑥 ∈ 𝐴 𝜓 ) ) )
17		reu5	⊢ ( ∃! 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ ∃* 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ) )
18		reu5	⊢ ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∃* 𝑥 ∈ 𝐴 𝜓 ) )
19	18	anbi2i	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) ↔ ( 𝜑 ∧ ( ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∃* 𝑥 ∈ 𝐴 𝜓 ) ) )
20	16 17 19	3imtr4i	⊢ ( ∃! 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) )
21		ibar	⊢ ( 𝜑 → ( 𝜓 ↔ ( 𝜑 ∧ 𝜓 ) ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 ↔ ( 𝜑 ∧ 𝜓 ) ) )
23	1 22	reubida	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐴 𝜓 ↔ ∃! 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ) )
24	23	biimpa	⊢ ( ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) → ∃! 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) )
25	20 24	impbii	⊢ ( ∃! 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ↔ ( 𝜑 ∧ ∃! 𝑥 ∈ 𝐴 𝜓 ) )