![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opeq1d | Structured version Visualization version GIF version |
Description: Equality deduction for ordered pairs. (Contributed by NM, 16-Dec-2006.) |
Ref | Expression |
---|---|
opeq1d.1 | ⊢ (𝜑 → 𝐴 = 𝐵) |
Ref | Expression |
---|---|
opeq1d | ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opeq1d.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐵) | |
2 | opeq1 4877 | . 2 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝜑 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1536 〈cop 4636 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-rab 3433 df-v 3479 df-dif 3965 df-un 3967 df-ss 3979 df-nul 4339 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 |
This theorem is referenced by: oteq1 4886 oteq2 4887 opth 5486 elsnxp 6312 cbvoprab2 7520 cbvoprab12v 7522 fvproj 8157 unxpdomlem1 9283 djulf1o 9949 djurf1o 9950 mulcanenq 10997 ax1rid 11198 axrnegex 11199 fseq1m1p1 13635 uzrdglem 13994 pfxswrd 14740 swrdccat 14769 swrdccat3blem 14773 cshw0 14828 cshwmodn 14829 s2prop 14942 s4prop 14945 fsum2dlem 15802 fprod2dlem 16012 ruclem1 16263 imasaddvallem 17575 iscatd2 17725 moni 17783 homadmcd 18095 curf1 18281 curf1cl 18284 curf2 18285 hofcl 18315 gsum2dlem2 20003 pzriprnglem10 21518 imasdsf1olem 24398 ovoliunlem1 25550 cxpcn3 26805 nosupbnd2 27775 noinfbnd2 27790 noseqrdglem 28325 axlowdimlem15 28985 axlowdim 28990 nvi 30642 nvop 30704 phop 30846 br8d 32629 fgreu 32688 1stpreimas 32720 rlocval 33245 rloccring 33256 smatfval 33755 smatrcl 33756 smatlem 33757 fmla0xp 35367 mvhfval 35517 mpst123 35524 br8 35735 fvtransport 36013 cbvoprab1vw 36219 cbvoprab2vw 36220 cbvoprab1davw 36253 cbvoprab2davw 36254 cbvoprab12davw 36257 bj-inftyexpitaudisj 37187 rfovcnvf1od 43993 |
Copyright terms: Public domain | W3C validator |