![]() |
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 2894 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V)) | |
2 | 1 | anbi1d 623 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V))) |
3 | sneq 4407 | . . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
4 | preq1 4486 | . . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) | |
5 | 3, 4 | preq12d 4494 | . . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}}) |
6 | 2, 5 | ifbieq1d 4329 | . 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)) |
7 | dfopif 4620 | . 2 ⊢ 〈𝐴, 𝐶〉 = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) | |
8 | dfopif 4620 | . 2 ⊢ 〈𝐵, 𝐶〉 = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅) | |
9 | 6, 7, 8 | 3eqtr4g 2886 | 1 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1656 ∈ wcel 2164 Vcvv 3414 ∅c0 4144 ifcif 4306 {csn 4397 {cpr 4399 〈cop 4403 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-13 2389 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-3an 1113 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-rab 3126 df-v 3416 df-dif 3801 df-un 3803 df-in 3805 df-ss 3812 df-nul 4145 df-if 4307 df-sn 4398 df-pr 4400 df-op 4404 |
This theorem is referenced by: opeq12 4625 opeq1i 4626 opeq1d 4629 oteq1 4632 breq1 4876 cbvopab1 4946 cbvopab1s 4948 opthg 5166 eqvinop 5175 opelopabsb 5211 opelxp 5378 elvvv 5411 opabid2 5484 opeliunxp2 5493 elsnres 5673 elimasng 5732 dmsnopg 5847 funopg 6157 f1osng 6418 f1oprswap 6421 dmfco 6519 fvelrn 6601 fsng 6654 funsneqopb 6670 fprg 6673 fvrnressn 6679 fvsngOLD 6701 funfvima3 6751 oveq1 6912 oprabid 6936 dfoprab2 6961 cbvoprab1 6987 elxp4 7372 elxp5 7373 opabex3d 7406 opabex3 7407 op1stg 7440 op2ndg 7441 el2xptp 7473 dfoprab4f 7488 frxp 7551 opeliunxp2f 7601 tfrlem11 7750 omeu 7932 oeeui 7949 elixpsn 8214 fundmen 8296 xpsnen 8313 xpassen 8323 xpf1o 8391 unxpdomlem1 8433 djur 9058 dfac5lem1 9259 dfac5lem4 9262 axdc4lem 9592 nqereu 10066 mulcanenq 10097 archnq 10117 prlem934 10170 supsrlem 10248 supsr 10249 swrdccatin1 13821 swrdccat3blem 13841 fsum2dlem 14876 fprod2dlem 15083 vdwlem10 16065 imasaddfnlem 16541 catideu 16688 iscatd2 16694 catlid 16696 catpropd 16721 symg2bas 18168 efgmval 18476 efgi 18483 vrgpval 18533 gsumcom2 18727 txkgen 21826 cnmpt21 21845 xkoinjcn 21861 txconn 21863 pt1hmeo 21980 cnextfvval 22239 qustgplem 22294 dvbsss 24065 axlowdim2 26259 axlowdim 26260 axcontlem10 26272 axcontlem12 26274 isnvlem 28009 br8d 29958 cnvoprabOLD 30035 prsrn 30495 esum2dlem 30688 eulerpartlemgvv 30972 br8 32177 br6 32178 br4 32179 eldm3 32182 dfdm5 32203 elfuns 32550 brimg 32572 brapply 32573 brsuccf 32576 brrestrict 32584 dfrdg4 32586 cgrdegen 32639 brofs 32640 cgrextend 32643 brifs 32678 ifscgr 32679 brcgr3 32681 brcolinear2 32693 colineardim1 32696 brfs 32714 idinside 32719 btwnconn1lem7 32728 btwnconn1lem11 32732 btwnconn1lem12 32733 brsegle 32743 outsideofeu 32766 fvray 32776 linedegen 32778 fvline 32779 bj-inftyexpiinv 33628 bj-inftyexpidisj 33630 finxpeq2 33762 finxpreclem6 33771 finxpsuclem 33772 curfv 33925 isdivrngo 34284 drngoi 34285 dicelval3 37248 dihjatcclem4 37489 dropab1 39482 relopabVD 39948 funressndmafv2rn 42118 dfatdmfcoafv2 42149 |
Copyright terms: Public domain | W3C validator |