Theorem opeq1 4805

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 2827	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4572	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4670	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4678	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4484	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4801	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4801	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107  Vcvv 3433  ∅c0 4257  ifcif 4460  {csn 4562  {cpr 4564  ⟨cop 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569

This theorem is referenced by:  opeq12  4807  opeq1i  4808  opeq1d  4811  oteq1  4814  breq1  5078  cbvopab1  5150  cbvopab1g  5151  cbvopab1s  5153  cbvopab1v  5154  opthg  5393  eqvinop  5402  sbcop1  5403  opelopabsb  5444  opelxp  5626  elvvv  5663  opabid2  5740  opeliunxp2  5750  elsnres  5934  elimasngOLD  6001  dmsnopg  6121  reuop  6200  funopg  6475  f1osng  6766  f1oprswap  6769  dmfco  6873  fvelrn  6963  fsng  7018  funsneqopb  7033  fprg  7036  fvrnressn  7042  funfvima3  7121  oveq1  7291  oprabidw  7315  oprabid  7316  dfoprab2  7342  cbvoprab1  7371  elxp4  7778  elxp5  7779  opabex3d  7817  opabex3rd  7818  opabex3  7819  op1stg  7852  op2ndg  7853  el2xptp  7886  dfoprab4f  7905  frxp  7976  opeliunxp2f  8035  tfrlem11  8228  omeu  8425  oeeui  8442  elixpsn  8734  fundmen  8830  xpsnen  8851  xpassen  8862  xpf1o  8935  unxpdomlem1  9036  djur  9686  dfac5lem1  9888  dfac5lem4  9891  axdc4lem  10220  nqereu  10694  mulcanenq  10725  archnq  10745  prlem934  10798  supsrlem  10876  supsr  10877  swrdccatin1  14447  swrdccat3blem  14461  fsum2dlem  15491  fprod2dlem  15699  vdwlem10  16700  imasaddfnlem  17248  catideu  17393  iscatd2  17399  catlid  17401  catpropd  17427  symg2bas  19009  efgmval  19327  efgi  19334  vrgpval  19382  gsumcom2  19585  txkgen  22812  cnmpt21  22831  xkoinjcn  22847  txconn  22849  pt1hmeo  22966  cnextfvval  23225  qustgplem  23281  dvbsss  25075  axlowdim2  27337  axlowdim  27338  axcontlem10  27350  axcontlem12  27352  isnvlem  28981  br8d  30959  2ndresdju  30995  cnvoprabOLD  31064  gsumhashmul  31325  prsrn  31874  esum2dlem  32069  eulerpartlemgvv  32352  fineqvrep  33073  satf0op  33348  satffunlem1lem1  33373  satffunlem2lem1  33375  sategoelfvb  33390  elxpxp  33692  br8  33732  br6  33733  br4  33734  eldm3  33737  dfdm5  33756  frxp2  33800  xpord2pred  33801  frxp3  33806  xpord3pred  33807  elfuns  34226  brimg  34248  brapply  34249  brsuccf  34252  brrestrict  34260  dfrdg4  34262  cgrdegen  34315  brofs  34316  cgrextend  34319  brifs  34354  ifscgr  34355  brcgr3  34357  brcolinear2  34369  colineardim1  34372  brfs  34390  idinside  34395  btwnconn1lem7  34404  btwnconn1lem11  34408  btwnconn1lem12  34409  brsegle  34419  outsideofeu  34442  fvray  34452  linedegen  34454  fvline  34455  bj-inftyexpiinv  35388  bj-inftyexpidisj  35390  finxpeq2  35567  finxpreclem6  35576  finxpsuclem  35577  curfv  35766  isdivrngo  36117  drngoi  36118  dicelval3  39201  dihjatcclem4  39442  dropab1  42072  relopabVD  42528  funressndmafv2rn  44726  dfatdmfcoafv2  44757  ichnreuop  44935  ichreuopeq  44936  reuopreuprim  44989  isthincd2lem2  46328