Theorem brsuccf

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

	Ref	Expression
Hypotheses	brsuccf.1	|- A e. _V
	brsuccf.2	|- B e. _V
Assertion	brsuccf	|- ( A Succ B <-> B = suc A )

Proof

Step	Hyp	Ref	Expression
1		brsuccf.1	|- A e. _V
2		brsuccf.2	|- B e. _V
3		df-succf	|- Succ = ( Cup o. ( _I (x) Singleton ) )
4	3	breqi	|- ( A Succ B <-> A ( Cup o. ( _I (x) Singleton ) ) B )
5	1 2	brco	|- ( A ( Cup o. ( _I (x) Singleton ) ) B <-> E. x ( A ( _I (x) Singleton ) x /\ x Cup B ) )
6	1 2	lemsuccf	|- ( E. x ( A ( _I (x) Singleton ) x /\ x Cup B ) <-> B = suc A )
7	4 5 6	3bitri	|- ( A Succ B <-> B = suc A )