Theorem ex-br

Description: Example for df-br . Example by David A. Wheeler. (Contributed by Mario Carneiro, 6-May-2015)

	Ref	Expression
Assertion	ex-br	|- ( R = { <. 2 , 6 >. , <. 3 , 9 >. } -> 3 R 9 )

Proof

Step	Hyp	Ref	Expression
1		opex	|- <. 3 , 9 >. e. _V
2	1	prid2	|- <. 3 , 9 >. e. { <. 2 , 6 >. , <. 3 , 9 >. }
3		id	|- ( R = { <. 2 , 6 >. , <. 3 , 9 >. } -> R = { <. 2 , 6 >. , <. 3 , 9 >. } )
4	2 3	eleqtrrid	|- ( R = { <. 2 , 6 >. , <. 3 , 9 >. } -> <. 3 , 9 >. e. R )
5		df-br	|- ( 3 R 9 <-> <. 3 , 9 >. e. R )
6	4 5	sylibr	|- ( R = { <. 2 , 6 >. , <. 3 , 9 >. } -> 3 R 9 )