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