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 ⊢ R = S ↾ C
Assertion eqres ⊢ B ∈ V → A R B ↔ A ∈ C ∧ A S B

Proof

Step Hyp Ref Expression
1 eqres.1 ⊢ R = S ↾ C
2 1 breqi ⊢ A R B ↔ A S ↾ C B
3 brres ⊢ B ∈ V → A S ↾ C B ↔ A ∈ C ∧ A S B
4 2 3 bitrid ⊢ B ∈ V → A R B ↔ A ∈ C ∧ A S B