**Description:** Equality theorem for a binary relation. (Contributed by NM, 31-Dec-1993)

Ref | Expression | ||
---|---|---|---|

Assertion | breq1 | ⊢ ( 𝐴 = 𝐵 → ( 𝐴 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | opeq1 | ⊢ ( 𝐴 = 𝐵 → ⟨ 𝐴 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) | |

2 | 1 | eleq1d | ⊢ ( 𝐴 = 𝐵 → ( ⟨ 𝐴 , 𝐶 ⟩ ∈ 𝑅 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) ) |

3 | df-br | ⊢ ( 𝐴 𝑅 𝐶 ↔ ⟨ 𝐴 , 𝐶 ⟩ ∈ 𝑅 ) | |

4 | df-br | ⊢ ( 𝐵 𝑅 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ 𝑅 ) | |

5 | 2 3 4 | 3bitr4g | ⊢ ( 𝐴 = 𝐵 → ( 𝐴 𝑅 𝐶 ↔ 𝐵 𝑅 𝐶 ) ) |