Theorem bnj602

Description: Equality theorem for the _pred function constant. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

	Ref	Expression
Assertion	bnj602	|- ( X = Y -> _pred ( X , A , R ) = _pred ( Y , A , R ) )

Proof

Step	Hyp	Ref	Expression
1		breq2	|- ( X = Y -> ( y R X <-> y R Y ) )
2	1	rabbidv	|- ( X = Y -> { y e. A | y R X } = { y e. A | y R Y } )
3		df-bnj14	|- _pred ( X , A , R ) = { y e. A | y R X }
4		df-bnj14	|- _pred ( Y , A , R ) = { y e. A | y R Y }
5	2 3 4	3eqtr4g	|- ( X = Y -> _pred ( X , A , R ) = _pred ( Y , A , R ) )