Theorem brsuccf

Description: Binary relation form of the Succ function. (Contributed by Scott Fenton, 14-Apr-2014)

	Ref	Expression
Hypotheses	brsuccf.1	⊢ 𝐴 ∈ V
	brsuccf.2	⊢ 𝐵 ∈ V
Assertion	brsuccf	⊢ ( 𝐴 Succ 𝐵 ↔ 𝐵 = suc 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		brsuccf.1	⊢ 𝐴 ∈ V
2		brsuccf.2	⊢ 𝐵 ∈ V
3		df-succf	⊢ Succ = ( Cup ∘ ( I ⊗ Singleton ) )
4	3	breqi	⊢ ( 𝐴 Succ 𝐵 ↔ 𝐴 ( Cup ∘ ( I ⊗ Singleton ) ) 𝐵 )
5	1 2	brco	⊢ ( 𝐴 ( Cup ∘ ( I ⊗ Singleton ) ) 𝐵 ↔ ∃ 𝑥 ( 𝐴 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝐵 ) )
6	1 2	lemsuccf	⊢ ( ∃ 𝑥 ( 𝐴 ( I ⊗ Singleton ) 𝑥 ∧ 𝑥 Cup 𝐵 ) ↔ 𝐵 = suc 𝐴 )
7	4 5 6	3bitri	⊢ ( 𝐴 Succ 𝐵 ↔ 𝐵 = suc 𝐴 )