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

Metamath Proof Explorer

Theorem eqres

Description: Converting a class constant definition by restriction (like df-ers or df-parts ) into a binary relation. (Contributed by Peter Mazsa, 1-Oct-2018)

		Ref	Expression
	Hypothesis	eqres.1	⊢ 𝑅 = ( 𝑆 ↾ 𝐶 )
	Assertion	eqres	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐴 𝑆 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqres.1	⊢ 𝑅 = ( 𝑆 ↾ 𝐶 )
2	1	breqi	⊢ ( 𝐴 𝑅 𝐵 ↔ 𝐴 ( 𝑆 ↾ 𝐶 ) 𝐵 )
3		brres	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ( 𝑆 ↾ 𝐶 ) 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐴 𝑆 𝐵 ) ) )
4	2 3	bitrid	⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 𝑅 𝐵 ↔ ( 𝐴 ∈ 𝐶 ∧ 𝐴 𝑆 𝐵 ) ) )