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 4804 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 〈cop 4567 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 |
This theorem is referenced by: axi2m1 10915 s3tpop 14622 2strstr1OLD 16938 2strop1 16940 grpbasex 17001 grpplusgx 17002 mat1dimelbas 21620 mat1dim0 21622 mat1dimid 21623 mat1dimscm 21624 mat1dimmul 21625 indistpsx 22160 setsiedg 27406 cusgrsize 27821 nosupcbv 33905 noinfcbv 33920 mapfzcons 40538 |
Copyright terms: Public domain | W3C validator |