Theorem opeq1 4854

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

Step	Hyp	Ref	Expression
1		eleq1 2823	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4616	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4714	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4722	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4530	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4851	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4851	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3464  ∅c0 4313  ifcif 4505  {csn 4606  {cpr 4608  ⟨cop 4612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613

This theorem is referenced by:  opeq12  4856  opeq1i  4857  opeq1d  4860  oteq1  4863  breq1  5127  cbvopab1  5198  cbvopab1g  5199  cbvopab1s  5201  cbvopab1v  5202  opthg  5457  eqvinop  5467  sbcop1  5468  opelopabsb  5510  opelxp  5695  elvvv  5735  opabid2  5812  opeliunxp2  5823  elsnres  6013  dmsnopg  6207  reuop  6287  funopg  6575  f1osng  6864  f1oprswap  6867  dmfco  6980  fvelrn  7071  fsng  7132  funsneqopb  7147  fprg  7150  fvrnressn  7156  funfvima3  7233  oveq1  7417  oprabidw  7441  oprabid  7442  dfoprab2  7470  cbvoprab1  7499  elxp4  7923  elxp5  7924  opabex3d  7969  opabex3rd  7970  opabex3  7971  op1stg  8005  op2ndg  8006  el2xptp  8039  dfoprab4f  8060  frxp  8130  frxp2  8148  xpord2pred  8149  opeliunxp2f  8214  tfrlem11  8407  omeu  8602  oeeui  8619  elixpsn  8956  fundmen  9050  xpsnen  9074  xpassen  9085  xpf1o  9158  unxpdomlem1  9263  djur  9938  dfac5lem1  10142  dfac5lem4  10145  dfac5lem4OLD  10147  axdc4lem  10474  nqereu  10948  mulcanenq  10979  archnq  10999  prlem934  11052  supsrlem  11130  supsr  11131  swrdccatin1  14748  swrdccat3blem  14762  fsum2dlem  15791  fprod2dlem  16001  vdwlem10  17015  imasaddfnlem  17547  catideu  17692  iscatd2  17698  catlid  17700  catpropd  17726  symg2bas  19379  efgmval  19698  efgi  19705  vrgpval  19753  gsumcom2  19961  rngqiprngimfo  21267  pzriprnglem10  21456  pzriprnglem11  21457  txkgen  23595  cnmpt21  23614  xkoinjcn  23630  txconn  23632  pt1hmeo  23749  cnextfvval  24008  qustgplem  24064  dvbsss  25860  axlowdim2  28944  axlowdim  28945  axcontlem10  28957  axcontlem12  28959  isnvlem  30596  br8d  32595  2ndresdju  32632  gsumhashmul  33060  gsumwrd2dccatlem  33065  rlocf1  33273  idomsubr  33308  prsrn  33951  esum2dlem  34128  eulerpartlemgvv  34413  fineqvrep  35131  satf0op  35404  satffunlem1lem1  35429  satffunlem2lem1  35431  sategoelfvb  35446  br8  35778  br6  35779  br4  35780  eldm3  35783  dfdm5  35795  elfuns  35938  brimg  35960  brapply  35961  brsuccf  35964  brrestrict  35972  dfrdg4  35974  cgrdegen  36027  brofs  36028  cgrextend  36031  brifs  36066  ifscgr  36067  brcgr3  36069  brcolinear2  36081  colineardim1  36084  brfs  36102  idinside  36107  btwnconn1lem7  36116  btwnconn1lem11  36120  btwnconn1lem12  36121  brsegle  36131  outsideofeu  36154  fvray  36164  linedegen  36166  fvline  36167  cbvoprab1vw  36260  cbvoprab13vw  36264  cbvopab1davw  36287  cbvoprab1davw  36294  bj-inftyexpiinv  37231  bj-inftyexpidisj  37233  finxpeq2  37410  finxpreclem6  37419  finxpsuclem  37420  curfv  37629  isdivrngo  37979  drngoi  37980  dicelval3  41204  dihjatcclem4  41445  dropab1  44438  relopabVD  44892  funressndmafv2rn  47219  dfatdmfcoafv2  47250  ichnreuop  47453  ichreuopeq  47454  reuopreuprim  47507  gpgedgvtx0  48032  gpgedgvtx1  48033  gpgcubic  48048  gpg5nbgr3star  48050  sectpropdlem  48970  ssccatid  49006  upfval2  49079  isthincd2lem2  49288