![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opeq2i | Structured version Visualization version GIF version |
Description: Equality inference for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
Ref | Expression |
---|---|
opeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
opeq2i | ⊢ 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | opeq2 4873 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 〈cop 4633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 |
This theorem is referenced by: fnressn 7152 fressnfv 7154 wfrlem14OLD 8318 seqomlem1 8446 recmulnq 10955 addresr 11129 seqval 13973 ids1 14543 pfx1 14649 pfxccatpfx2 14683 ressinbas 17186 oduval 18237 mgmnsgrpex 18808 sgrpnmndex 18809 efgi0 19582 efgi1 19583 vrgpinv 19631 frgpnabllem1 19735 mat1dimid 21967 uspgr1v1eop 28495 wlk2v2e 29399 avril1 29705 nvop 29916 phop 30058 bnj601 33919 tgrpset 39604 erngset 39659 erngset-rN 39667 zlmodzxzadd 46987 lmod1 47126 lmod1zr 47127 zlmodzxzequa 47130 zlmodzxzequap 47133 |
Copyright terms: Public domain | W3C validator |