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

Metamath Proof Explorer

Theorem breq2dd

Description: Equality deduction for a binary relation. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses breq2dd.1 ⊢ φ → A = B
breq2dd.2 ⊢ φ → C R A
Assertion breq2dd ⊢ φ → C R B

Proof

Step Hyp Ref Expression
1 breq2dd.1 ⊢ φ → A = B
2 breq2dd.2 ⊢ φ → C R A
3 1 breq2d ⊢ φ → C R A ↔ C R B
4 2 3 mpbid ⊢ φ → C R B