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