Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opeq2 | Structured version Visualization version GIF version |
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
opeq2 | ⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2897 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V)) | |
2 | 1 | anbi2d 628 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V))) |
3 | preq2 4662 | . . . 4 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | |
4 | 3 | preq2d 4668 | . . 3 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}}) |
5 | 2, 4 | ifbieq1d 4486 | . 2 ⊢ (𝐴 = 𝐵 → if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅)) |
6 | dfopif 4792 | . 2 ⊢ 〈𝐶, 𝐴〉 = if((𝐶 ∈ V ∧ 𝐴 ∈ V), {{𝐶}, {𝐶, 𝐴}}, ∅) | |
7 | dfopif 4792 | . 2 ⊢ 〈𝐶, 𝐵〉 = if((𝐶 ∈ V ∧ 𝐵 ∈ V), {{𝐶}, {𝐶, 𝐵}}, ∅) | |
8 | 5, 6, 7 | 3eqtr4g 2878 | 1 ⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ wcel 2105 Vcvv 3492 ∅c0 4288 ifcif 4463 {csn 4557 {cpr 4559 〈cop 4563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 |
This theorem is referenced by: opeq12 4797 opeq2i 4799 opeq2d 4802 oteq2 4805 oteq3 4806 breq2 5061 cbvopab2 5132 cbvopab2v 5135 opthg 5360 eqvinop 5369 opelopabsb 5408 dfid3 5455 opelxp 5584 relopabi 5687 opabid2 5693 elrn2g 5754 opeldmd 5768 opeldm 5769 elrn2 5814 iss 5896 elidinxp 5904 elimasng 5948 dmsnopg 6063 reuop 6137 funopg 6382 f1osng 6648 f1oprswap 6651 tz6.12f 6687 fvn0ssdmfun 6834 fsn 6889 fsng 6891 fprg 6909 fprb 6948 oveq2 7153 cbvoprab2 7231 ovg 7302 elxp4 7616 elxp5 7617 opabex3d 7655 opabex3rd 7656 opabex3 7657 op1stg 7690 op2ndg 7691 op1steq 7722 dfoprab4f 7743 fsplit 7801 seqomlem2 8076 omeu 8200 oeeui 8217 ralxpmap 8448 elixpsn 8489 ixpsnf1o 8490 mapsnend 8576 xpsnen 8589 xpassen 8599 xpf1o 8667 unxpdomlem1 8710 djulcl 9327 djurcl 9328 djur 9336 djuss 9337 djuun 9343 1stinl 9344 2ndinl 9345 1stinr 9346 2ndinr 9347 axdc4lem 9865 nqereu 10339 mulcanenq 10370 elreal 10541 ax1rid 10571 fseq1p1m1 12969 pfxval 14023 swrdccatin1 14075 swrdccat3blem 14089 wrdlen2 14294 ruclem1 15572 imasaddfnlem 16789 imasvscafn 16798 catidex 16933 catpropd 16967 funcsetcestrclem1 17392 symg2bas 18455 efgi 18774 gsumcom2 19024 mat1rhmval 21016 mat1ric 21024 txkgen 22188 cnmpt21 22207 xkoinjcn 22223 txconn 22225 xpstopnlem1 22345 qustgplem 22656 metustid 23091 axlowdim2 26673 axlowdim 26674 axcontlem2 26678 axcontlem3 26679 axcontlem4 26680 axcontlem9 26685 axcontlem10 26686 axcontlem11 26687 cusgrexg 27153 rgrusgrprc 27298 2clwwlk2clwwlk 28056 isnvlem 28314 br8d 30289 prsdm 31056 eulerpartlemgvv 31533 reprsuc 31785 bnj941 31943 bnj944 32109 cvmlift2lem1 32446 cvmlift2lem12 32458 goel 32491 gonafv 32494 satf0op 32521 sat1el2xp 32523 fmla0xp 32527 sategoelfvb 32563 br8 32889 br6 32890 br4 32891 dfrn5 32914 elima4 32916 pprodss4v 33242 brimg 33295 brapply 33296 brsuccf 33299 brrestrict 33307 dfrdg4 33309 cgrtriv 33360 brofs 33363 segconeu 33369 btwntriv2 33370 transportprops 33392 brifs 33401 ifscgr 33402 brcgr3 33404 cgrxfr 33413 brcolinear2 33416 colineardim1 33419 brfs 33437 idinside 33442 btwnconn1lem7 33451 btwnconn1lem11 33455 btwnconn1lem12 33456 btwnconn1lem14 33458 brsegle 33466 seglerflx 33470 seglemin 33471 segleantisym 33473 btwnsegle 33475 outsideofeu 33489 outsidele 33490 linedegen 33501 fvline 33502 finxpreclem6 34559 finxpsuclem 34560 curfv 34753 poimirlem4 34777 poimirlem26 34799 isdivrngo 35109 drngoi 35110 iss2 35482 dibelval3 38163 diblsmopel 38187 dihjatcclem4 38437 frlmsnic 39027 dfhe3 39999 dffrege115 40202 dropab2 40657 relopabVD 41112 projf1o 41335 sge0xp 42588 hoidmv1le 42753 ichnreuop 43511 ichreuopeq 43512 reuopreuprim 43565 prelrrx2b 44629 rrx2xpref1o 44633 rrx2plordisom 44638 |
Copyright terms: Public domain | W3C validator |