Theorem mo5f

Description: Alternate definition of "at most one." (Contributed by Thierry Arnoux, 1-Mar-2017)

	Ref	Expression
Hypotheses	mo5f.1	⊢ Ⅎ 𝑖 𝜑
	mo5f.2	⊢ Ⅎ 𝑗 𝜑
Assertion	mo5f	⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑖 ∀ 𝑗 ( ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑖 = 𝑗 ) )

Proof

Step	Hyp	Ref	Expression
1		mo5f.1	⊢ Ⅎ 𝑖 𝜑
2		mo5f.2	⊢ Ⅎ 𝑗 𝜑
3	2	mo3	⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑥 ∀ 𝑗 ( ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑗 ) )
4	1	nfsbv	⊢ Ⅎ 𝑖 [ 𝑗 / 𝑥 ] 𝜑
5	1 4	nfan	⊢ Ⅎ 𝑖 ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 )
6		nfv	⊢ Ⅎ 𝑖 𝑥 = 𝑗
7	5 6	nfim	⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑗 )
8	7	nfal	⊢ Ⅎ 𝑖 ∀ 𝑗 ( ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑗 )
9	8	sb8f	⊢ ( ∀ 𝑥 ∀ 𝑗 ( ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑗 ) ↔ ∀ 𝑖 [ 𝑖 / 𝑥 ] ∀ 𝑗 ( ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑗 ) )
10		sbim	⊢ ( [ 𝑖 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑗 ) ↔ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → [ 𝑖 / 𝑥 ] 𝑥 = 𝑗 ) )
11		sban	⊢ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑖 / 𝑥 ] [ 𝑗 / 𝑥 ] 𝜑 ) )
12		nfs1v	⊢ Ⅎ 𝑥 [ 𝑗 / 𝑥 ] 𝜑
13	12	sbf	⊢ ( [ 𝑖 / 𝑥 ] [ 𝑗 / 𝑥 ] 𝜑 ↔ [ 𝑗 / 𝑥 ] 𝜑 )
14	13	bicomi	⊢ ( [ 𝑗 / 𝑥 ] 𝜑 ↔ [ 𝑖 / 𝑥 ] [ 𝑗 / 𝑥 ] 𝜑 )
15	14	anbi2i	⊢ ( ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑖 / 𝑥 ] [ 𝑗 / 𝑥 ] 𝜑 ) )
16	11 15	bitr4i	⊢ ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) )
17		equsb3	⊢ ( [ 𝑖 / 𝑥 ] 𝑥 = 𝑗 ↔ 𝑖 = 𝑗 )
18	16 17	imbi12i	⊢ ( ( [ 𝑖 / 𝑥 ] ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → [ 𝑖 / 𝑥 ] 𝑥 = 𝑗 ) ↔ ( ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑖 = 𝑗 ) )
19	10 18	bitri	⊢ ( [ 𝑖 / 𝑥 ] ( ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑗 ) ↔ ( ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑖 = 𝑗 ) )
20	19	sbalv	⊢ ( [ 𝑖 / 𝑥 ] ∀ 𝑗 ( ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑗 ) ↔ ∀ 𝑗 ( ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑖 = 𝑗 ) )
21	20	albii	⊢ ( ∀ 𝑖 [ 𝑖 / 𝑥 ] ∀ 𝑗 ( ( 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑥 = 𝑗 ) ↔ ∀ 𝑖 ∀ 𝑗 ( ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑖 = 𝑗 ) )
22	3 9 21	3bitri	⊢ ( ∃* 𝑥 𝜑 ↔ ∀ 𝑖 ∀ 𝑗 ( ( [ 𝑖 / 𝑥 ] 𝜑 ∧ [ 𝑗 / 𝑥 ] 𝜑 ) → 𝑖 = 𝑗 ) )