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