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	⊢ Ⅎ 𝑥 𝑅
	dfrel4.2	⊢ Ⅎ 𝑦 𝑅
Assertion	dfrel4	⊢ ( Rel 𝑅 ↔ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } )

Proof

Step	Hyp	Ref	Expression
1		dfrel4.1	⊢ Ⅎ 𝑥 𝑅
2		dfrel4.2	⊢ Ⅎ 𝑦 𝑅
3		dfrel4v	⊢ ( Rel 𝑅 ↔ 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 𝑅 𝑏 } )
4		nfcv	⊢ Ⅎ 𝑥 𝑎
5		nfcv	⊢ Ⅎ 𝑥 𝑏
6	4 1 5	nfbr	⊢ Ⅎ 𝑥 𝑎 𝑅 𝑏
7		nfcv	⊢ Ⅎ 𝑦 𝑎
8		nfcv	⊢ Ⅎ 𝑦 𝑏
9	7 2 8	nfbr	⊢ Ⅎ 𝑦 𝑎 𝑅 𝑏
10		nfv	⊢ Ⅎ 𝑎 𝑥 𝑅 𝑦
11		nfv	⊢ Ⅎ 𝑏 𝑥 𝑅 𝑦
12		breq12	⊢ ( ( 𝑎 = 𝑥 ∧ 𝑏 = 𝑦 ) → ( 𝑎 𝑅 𝑏 ↔ 𝑥 𝑅 𝑦 ) )
13	6 9 10 11 12	cbvopab	⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 𝑅 𝑏 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 }
14	13	eqeq2i	⊢ ( 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 𝑅 𝑏 } ↔ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } )
15	3 14	bitri	⊢ ( Rel 𝑅 ↔ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝑅 𝑦 } )

Metamath Proof Explorer

Theorem dfrel4

Proof