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

Metamath Proof Explorer

Theorem rmo4f

Description: Restricted "at most one" using implicit substitution. (Contributed by NM, 24-Oct-2006) (Revised by Thierry Arnoux, 11-Oct-2016) (Revised by Thierry Arnoux, 8-Mar-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

Ref Expression
Hypotheses rmo4f.1 ⊢ Ⅎ 𝑥 𝐴
rmo4f.2 ⊢ Ⅎ 𝑦 𝐴
rmo4f.3 ⊢ Ⅎ 𝑥 𝜓
rmo4f.4 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion rmo4f ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 rmo4f.1 ⊢ Ⅎ 𝑥 𝐴
2 rmo4f.2 ⊢ Ⅎ 𝑦 𝐴
3 rmo4f.3 ⊢ Ⅎ 𝑥 𝜓
4 rmo4f.4 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
5 nfv ⊢ Ⅎ 𝑦 𝜑
6 1 2 5 rmo3f ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) )
7 3 4 sbiev ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜓 )
8 7 anbi2i ⊢ ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( 𝜑 ∧ 𝜓 ) )
9 8 imbi1i ⊢ ( ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
10 9 2ralbii ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ [ 𝑦 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )
11 6 10 bitri ⊢ ( ∃* 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝜑 ∧ 𝜓 ) → 𝑥 = 𝑦 ) )