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=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to 3R9$$

Proof

Step	Hyp	Ref	Expression
1		opex	$$⊢⟨3,9⟩\in \mathrm{V}$$
2	1	prid2	$$⊢⟨3,9⟩\in \left\{⟨2,6⟩,⟨3,9⟩\right\}$$
3		id	$$⊢R=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to R=\left\{⟨2,6⟩,⟨3,9⟩\right\}$$
4	2 3	eleqtrrid	$$⊢R=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to ⟨3,9⟩\in R$$
5		df-br	$$⊢3R9\leftrightarrow ⟨3,9⟩\in R$$
6	4 5	sylibr	$$⊢R=\left\{⟨2,6⟩,⟨3,9⟩\right\}\to 3R9$$