Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opeq1i | Structured version Visualization version GIF version |
Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
Ref | Expression |
---|---|
opeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
opeq1i | ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | opeq1 4759 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 〈cop 4522 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2020 ax-8 2116 ax-9 2124 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-ex 1787 df-sb 2075 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3400 df-un 3848 df-sn 4517 df-pr 4519 df-op 4523 |
This theorem is referenced by: axi2m1 10661 s3tpop 14362 2strstr1 16710 2strop1 16712 grpbasex 16718 grpplusgx 16719 mat1dimelbas 21224 mat1dim0 21226 mat1dimid 21227 mat1dimscm 21228 mat1dimmul 21229 indistpsx 21763 setsiedg 26983 cusgrsize 27398 nosupcbv 33550 noinfcbv 33565 mapfzcons 40132 |
Copyright terms: Public domain | W3C validator |