**Description:** Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006)

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

Hypothesis | opeq1i.1 | ⊢ 𝐴 = 𝐵 | |

Assertion | opeq1i | ⊢ ⟨ 𝐴 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ |

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

1 | opeq1i.1 | ⊢ 𝐴 = 𝐵 | |

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

3 | 1 2 | ax-mp | ⊢ ⟨ 𝐴 , 𝐶 ⟩ = ⟨ 𝐵 , 𝐶 ⟩ |