This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfrel4

Description: A relation can be expressed as the set of ordered pairs in it. An analogue of dffn5 for relations. (Contributed by Mario Carneiro, 16-Aug-2015) (Revised by Thierry Arnoux, 11-May-2017)

Ref Expression
Hypotheses dfrel4.1 ⊢ Ⅎ _ x R
dfrel4.2 ⊢ Ⅎ _ y R
Assertion dfrel4 ⊢ Rel ⁡ R ↔ R = x y | x R y

Proof

Step Hyp Ref Expression
1 dfrel4.1 ⊢ Ⅎ _ x R
2 dfrel4.2 ⊢ Ⅎ _ y R
3 dfrel4v ⊢ Rel ⁡ R ↔ R = a b | a R b
4 nfcv ⊢ Ⅎ _ x a
5 nfcv ⊢ Ⅎ _ x b
6 4 1 5 nfbr ⊢ Ⅎ x a R b
7 nfcv ⊢ Ⅎ _ y a
8 nfcv ⊢ Ⅎ _ y b
9 7 2 8 nfbr ⊢ Ⅎ y a R b
10 nfv ⊢ Ⅎ a x R y
11 nfv ⊢ Ⅎ b x R y
12 breq12 ⊢ a = x ∧ b = y → a R b ↔ x R y
13 6 9 10 11 12 cbvopab ⊢ a b | a R b = x y | x R y
14 13 eqeq2i ⊢ R = a b | a R b ↔ R = x y | x R y
15 3 14 bitri ⊢ Rel ⁡ R ↔ R = x y | x R y