Theorem brab1

Description: Relationship between a binary relation and a class abstraction. (Contributed by Andrew Salmon, 8-Jul-2011)

	Ref	Expression
Assertion	brab1	|- ( x R A <-> x e. { z | z R A } )

Proof

Step	Hyp	Ref	Expression
1		breq1	|- ( z = y -> ( z R A <-> y R A ) )
2		breq1	|- ( y = x -> ( y R A <-> x R A ) )
3	1 2	sbcie2g	|- ( x e. _V -> ( [. x / z ]. z R A <-> x R A ) )
4	3	elv	|- ( [. x / z ]. z R A <-> x R A )
5		df-sbc	|- ( [. x / z ]. z R A <-> x e. { z | z R A } )
6	4 5	bitr3i	|- ( x R A <-> x e. { z | z R A } )