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 2676 | . . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V)) | |
2 | 1 | anbi1d 737 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V))) |
3 | sneq 4135 | . . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
4 | preq1 4212 | . . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) | |
5 | 3, 4 | preq12d 4220 | . . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}}) |
6 | 2, 5 | ifbieq1d 4059 | . 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)) |
7 | dfopif 4337 | . 2 ⊢ 〈𝐴, 𝐶〉 = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) | |
8 | dfopif 4337 | . 2 ⊢ 〈𝐵, 𝐶〉 = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅) | |
9 | 6, 7, 8 | 3eqtr4g 2669 | 1 ⊢ (𝐴 = 𝐵 → 〈𝐴, 𝐶〉 = 〈𝐵, 𝐶〉) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 = wceq 1475 ∈ wcel 1977 Vcvv 3173 ∅c0 3874 ifcif 4036 {csn 4125 {cpr 4127 〈cop 4131 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 |
This theorem is referenced by: opeq12 4342 opeq1i 4343 opeq1d 4346 oteq1 4349 breq1 4586 cbvopab1 4655 cbvopab1s 4657 opthg 4872 eqvinop 4881 opelopabsb 4910 opelxp 5070 elvvv 5101 opabid2 5173 opeliunxp2 5182 elsnres 5356 elimasng 5410 dmsnopg 5524 cnvsng 5539 elsnxpOLD 5595 funopg 5836 f1osng 6089 f1oprswap 6092 dmfco 6182 fvelrn 6260 fsng 6310 fprg 6327 fvrnressn 6333 fvsng 6352 funfvima3 6399 oveq1 6556 oprabid 6576 dfoprab2 6599 cbvoprab1 6625 elxp4 7003 elxp5 7004 opabex3d 7037 opabex3 7038 op1stg 7071 op2ndg 7072 el2xptp 7102 dfoprab4f 7117 frxp 7174 opeliunxp2f 7223 tfrlem11 7371 omeu 7552 oeeui 7569 elixpsn 7833 fundmen 7916 xpsnen 7929 xpassen 7939 xpf1o 8007 unxpdomlem1 8049 dfac5lem1 8829 dfac5lem4 8832 axdc4lem 9160 nqereu 9630 mulcanenq 9661 archnq 9681 prlem934 9734 supsrlem 9811 supsr 9812 swrdccatin1 13334 swrdccat3blem 13346 fsum2dlem 14343 fprod2dlem 14549 vdwlem10 15532 imasaddfnlem 16011 catideu 16159 iscatd2 16165 catlid 16167 catpropd 16192 symg2bas 17641 efgmval 17948 efgi 17955 vrgpval 18003 gsumcom2 18197 txkgen 21265 cnmpt21 21284 xkoinjcn 21300 txcon 21302 pt1hmeo 21419 cnextfvval 21679 qustgplem 21734 dvbsss 23472 axlowdim2 25640 axlowdim 25641 axcontlem10 25653 axcontlem12 25655 0eusgraiff0rgra 26466 isnvlem 26849 br8d 28802 cnvoprab 28886 prsrn 29289 esum2dlem 29481 eulerpartlemgvv 29765 br8 30899 br6 30900 br4 30901 eldm3 30905 br1steqg 30919 br2ndeqg 30920 dfdm5 30921 elfuns 31192 brimg 31214 brapply 31215 brsuccf 31218 brrestrict 31226 dfrdg4 31228 cgrdegen 31281 brofs 31282 cgrextend 31285 brifs 31320 ifscgr 31321 brcgr3 31323 brcolinear2 31335 colineardim1 31338 brfs 31356 idinside 31361 btwnconn1lem7 31370 btwnconn1lem11 31374 btwnconn1lem12 31375 brsegle 31385 outsideofeu 31408 fvray 31418 linedegen 31420 fvline 31421 bj-inftyexpiinv 32272 bj-inftyexpidisj 32274 finxpeq2 32400 finxpreclem6 32409 finxpsuclem 32410 curfv 32559 isdivrngo 32919 drngoi 32920 dicelval3 35487 dihjatcclem4 35728 dropab1 37672 relopabVD 38159 |
Copyright terms: Public domain | W3C validator |