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	⊢ ( 𝑅 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → 3 𝑅 9 )

Proof

Step	Hyp	Ref	Expression
1		opex	⊢ ⟨ 3 , 9 ⟩ ∈ V
2	1	prid2	⊢ ⟨ 3 , 9 ⟩ ∈ { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ }
3		id	⊢ ( 𝑅 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → 𝑅 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } )
4	2 3	eleqtrrid	⊢ ( 𝑅 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → ⟨ 3 , 9 ⟩ ∈ 𝑅 )
5		df-br	⊢ ( 3 𝑅 9 ↔ ⟨ 3 , 9 ⟩ ∈ 𝑅 )
6	4 5	sylibr	⊢ ( 𝑅 = { ⟨ 2 , 6 ⟩ , ⟨ 3 , 9 ⟩ } → 3 𝑅 9 )