Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  opeq1 Structured version   Visualization version   GIF version

Theorem opeq1 4377
 Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opeq1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Proof of Theorem opeq1
StepHypRef Expression
1 eleq1 2686 . . . 4 (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
21anbi1d 740 . . 3 (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3 sneq 4165 . . . 4 (𝐴 = 𝐵 → {𝐴} = {𝐵})
4 preq1 4245 . . . 4 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
53, 4preq12d 4253 . . 3 (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
62, 5ifbieq1d 4087 . 2 (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7 dfopif 4374 . 2 𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8 dfopif 4374 . 2 𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
96, 7, 83eqtr4g 2680 1 (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  Vcvv 3190  ∅c0 3897  ifcif 4064  {csn 4155  {cpr 4157  ⟨cop 4161 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rab 2917  df-v 3192  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162 This theorem is referenced by:  opeq12  4379  opeq1i  4380  opeq1d  4383  oteq1  4386  breq1  4626  cbvopab1  4695  cbvopab1s  4697  opthg  4916  eqvinop  4925  opelopabsb  4955  opelxp  5116  elvvv  5149  opabid2  5221  opeliunxp2  5230  elsnres  5405  elimasng  5460  dmsnopg  5575  cnvsng  5590  elsnxpOLD  5647  funopg  5890  f1osng  6144  f1oprswap  6147  dmfco  6239  fvelrn  6318  fsng  6369  fprg  6387  fvrnressn  6393  fvsng  6412  funfvima3  6460  oveq1  6622  oprabid  6642  dfoprab2  6666  cbvoprab1  6692  elxp4  7072  elxp5  7073  opabex3d  7106  opabex3  7107  op1stg  7140  op2ndg  7141  el2xptp  7171  dfoprab4f  7186  frxp  7247  opeliunxp2f  7296  tfrlem11  7444  omeu  7625  oeeui  7642  elixpsn  7907  fundmen  7990  xpsnen  8004  xpassen  8014  xpf1o  8082  unxpdomlem1  8124  dfac5lem1  8906  dfac5lem4  8909  axdc4lem  9237  nqereu  9711  mulcanenq  9742  archnq  9762  prlem934  9815  supsrlem  9892  supsr  9893  swrdccatin1  13436  swrdccat3blem  13448  fsum2dlem  14448  fprod2dlem  14654  vdwlem10  15637  imasaddfnlem  16128  catideu  16276  iscatd2  16282  catlid  16284  catpropd  16309  symg2bas  17758  efgmval  18065  efgi  18072  vrgpval  18120  gsumcom2  18314  txkgen  21395  cnmpt21  21414  xkoinjcn  21430  txconn  21432  pt1hmeo  21549  cnextfvval  21809  qustgplem  21864  dvbsss  23606  axlowdim2  25774  axlowdim  25775  axcontlem10  25787  axcontlem12  25789  isnvlem  27353  br8d  29306  cnvoprab  29382  prsrn  29785  esum2dlem  29977  eulerpartlemgvv  30261  br8  31407  br6  31408  br4  31409  eldm3  31413  br1steqg  31429  br2ndeqg  31430  dfdm5  31431  elfuns  31717  brimg  31739  brapply  31740  brsuccf  31743  brrestrict  31751  dfrdg4  31753  cgrdegen  31806  brofs  31807  cgrextend  31810  brifs  31845  ifscgr  31846  brcgr3  31848  brcolinear2  31860  colineardim1  31863  brfs  31881  idinside  31886  btwnconn1lem7  31895  btwnconn1lem11  31899  btwnconn1lem12  31900  brsegle  31910  outsideofeu  31933  fvray  31943  linedegen  31945  fvline  31946  bj-inftyexpiinv  32767  bj-inftyexpidisj  32769  finxpeq2  32895  finxpreclem6  32904  finxpsuclem  32905  curfv  33060  isdivrngo  33420  drngoi  33421  dicelval3  35988  dihjatcclem4  36229  dropab1  38172  relopabVD  38659
 Copyright terms: Public domain W3C validator