Theorem brab1

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

	Ref	Expression
Assertion	brab1	$$⊢xRA\leftrightarrow x\in \left\{z|zRA\right\}$$

Proof

Step	Hyp	Ref	Expression
1		breq1	$$⊢z=y\to \left(zRA\leftrightarrow yRA\right)$$
2		breq1	$$⊢y=x\to \left(yRA\leftrightarrow xRA\right)$$
3	1 2	sbcie2g	$$⊢x\in \mathrm{V}\to \left(\underset{\dot{}}{[}x/z\underset{\dot{}}{]}zRA\leftrightarrow xRA\right)$$
4	3	elv	$$⊢\underset{\dot{}}{[}x/z\underset{\dot{}}{]}zRA\leftrightarrow xRA$$
5		df-sbc	$$⊢\underset{\dot{}}{[}x/z\underset{\dot{}}{]}zRA\leftrightarrow x\in \left\{z|zRA\right\}$$
6	4 5	bitr3i	$$⊢xRA\leftrightarrow x\in \left\{z|zRA\right\}$$