Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opeq1 | 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 |
---|---|
opeq1 | ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2897 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V)) | |
2 | 1 | anbi1d 629 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V))) |
3 | sneq 4567 | . . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
4 | preq1 4661 | . . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) | |
5 | 3, 4 | preq12d 4669 | . . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}}) |
6 | 2, 5 | ifbieq1d 4486 | . 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)) |
7 | dfopif 4792 | . 2 ⊢ 〈𝐴, 𝐶〉 = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) | |
8 | dfopif 4792 | . 2 ⊢ 〈𝐵, 𝐶〉 = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅) | |
9 | 6, 7, 8 | 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 opeq1i 4798 opeq1d 4801 oteq1 4804 breq1 5060 cbvopab1 5130 cbvopab1g 5131 cbvopab1s 5133 opthg 5360 eqvinop 5369 sbcop1 5370 opelopabsb 5408 opelxp 5584 elvvv 5620 opabid2 5693 opeliunxp2 5702 elsnres 5885 elimasng 5948 dmsnopg 6063 reuop 6137 funopg 6382 f1osng 6648 f1oprswap 6651 dmfco 6750 fvelrn 6836 fsng 6891 funsneqopb 6906 fprg 6909 fvrnressn 6915 funfvima3 6989 oveq1 7152 oprabidw 7176 oprabid 7177 dfoprab2 7201 cbvoprab1 7230 elxp4 7616 elxp5 7617 opabex3d 7655 opabex3rd 7656 opabex3 7657 op1stg 7690 op2ndg 7691 el2xptp 7724 dfoprab4f 7743 frxp 7809 opeliunxp2f 7865 tfrlem11 8013 omeu 8200 oeeui 8217 elixpsn 8489 fundmen 8571 xpsnen 8589 xpassen 8599 xpf1o 8667 unxpdomlem1 8710 djur 9336 dfac5lem1 9537 dfac5lem4 9540 axdc4lem 9865 nqereu 10339 mulcanenq 10370 archnq 10390 prlem934 10443 supsrlem 10521 supsr 10522 swrdccatin1 14075 swrdccat3blem 14089 fsum2dlem 15113 fprod2dlem 15322 vdwlem10 16314 imasaddfnlem 16789 catideu 16934 iscatd2 16940 catlid 16942 catpropd 16967 symg2bas 18455 efgmval 18767 efgi 18774 vrgpval 18822 gsumcom2 19024 txkgen 22188 cnmpt21 22207 xkoinjcn 22223 txconn 22225 pt1hmeo 22342 cnextfvval 22601 qustgplem 22656 dvbsss 24427 axlowdim2 26673 axlowdim 26674 axcontlem10 26686 axcontlem12 26688 isnvlem 28314 br8d 30289 cnvoprabOLD 30382 prsrn 31057 esum2dlem 31250 eulerpartlemgvv 31533 satf0op 32521 satffunlem1lem1 32546 satffunlem2lem1 32548 sategoelfvb 32563 br8 32889 br6 32890 br4 32891 eldm3 32894 dfdm5 32913 elfuns 33273 brimg 33295 brapply 33296 brsuccf 33299 brrestrict 33307 dfrdg4 33309 cgrdegen 33362 brofs 33363 cgrextend 33366 brifs 33401 ifscgr 33402 brcgr3 33404 brcolinear2 33416 colineardim1 33419 brfs 33437 idinside 33442 btwnconn1lem7 33451 btwnconn1lem11 33455 btwnconn1lem12 33456 brsegle 33466 outsideofeu 33489 fvray 33499 linedegen 33501 fvline 33502 bj-inftyexpiinv 34382 bj-inftyexpidisj 34384 finxpeq2 34550 finxpreclem6 34559 finxpsuclem 34560 curfv 34753 isdivrngo 35109 drngoi 35110 dicelval3 38196 dihjatcclem4 38437 dropab1 40656 relopabVD 41112 funressndmafv2rn 43299 dfatdmfcoafv2 43330 ichnreuop 43511 ichreuopeq 43512 reuopreuprim 43565 |
Copyright terms: Public domain | W3C validator |