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

Metamath Proof Explorer

Theorem reupick2

Description: Restricted uniqueness "picks" a member of a subclass. (Contributed by Mario Carneiro, 15-Dec-2013) (Proof shortened by Mario Carneiro, 19-Nov-2016)

Ref Expression
Assertion reupick2 ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 ancr ⊢ ( ( 𝜓 → 𝜑 ) → ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) )
2 1 ralimi ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) → ∀ 𝑥 ∈ 𝐴 ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) )
3 rexim ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → ( 𝜑 ∧ 𝜓 ) ) → ( ∃ 𝑥 ∈ 𝐴 𝜓 → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ) )
4 2 3 syl ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) → ( ∃ 𝑥 ∈ 𝐴 𝜓 → ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ) )
5 reupick3 ⊢ ( ( ∃! 𝑥 ∈ 𝐴 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 → 𝜓 ) )
6 5 3exp ⊢ ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) ) )
7 6 com12 ⊢ ( ∃ 𝑥 ∈ 𝐴 ( 𝜑 ∧ 𝜓 ) → ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) ) )
8 4 7 syl6 ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) → ( ∃ 𝑥 ∈ 𝐴 𝜓 → ( ∃! 𝑥 ∈ 𝐴 𝜑 → ( 𝑥 ∈ 𝐴 → ( 𝜑 → 𝜓 ) ) ) ) )
9 8 3imp1 ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 → 𝜓 ) )
10 rsp ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜑 ) ) )
11 10 3ad2ant1 ⊢ ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) → ( 𝑥 ∈ 𝐴 → ( 𝜓 → 𝜑 ) ) )
12 11 imp ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜓 → 𝜑 ) )
13 9 12 impbid ⊢ ( ( ( ∀ 𝑥 ∈ 𝐴 ( 𝜓 → 𝜑 ) ∧ ∃ 𝑥 ∈ 𝐴 𝜓 ∧ ∃! 𝑥 ∈ 𝐴 𝜑 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝜑 ↔ 𝜓 ) )