Theorem opeq1 4801

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 2826	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 629	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4568	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4666	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4674	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4480	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4797	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4797	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2804	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  Vcvv 3422  ∅c0 4253  ifcif 4456  {csn 4558  {cpr 4560  ⟨cop 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565

This theorem is referenced by:  opeq12  4803  opeq1i  4804  opeq1d  4807  oteq1  4810  breq1  5073  cbvopab1  5145  cbvopab1g  5146  cbvopab1s  5148  cbvopab1v  5149  opthg  5386  eqvinop  5395  sbcop1  5396  opelopabsb  5436  opelxp  5616  elvvv  5653  opabid2  5727  opeliunxp2  5736  elsnres  5920  elimasngOLD  5987  dmsnopg  6105  reuop  6185  funopg  6452  f1osng  6740  f1oprswap  6743  dmfco  6846  fvelrn  6936  fsng  6991  funsneqopb  7006  fprg  7009  fvrnressn  7015  funfvima3  7094  oveq1  7262  oprabidw  7286  oprabid  7287  dfoprab2  7311  cbvoprab1  7340  elxp4  7743  elxp5  7744  opabex3d  7781  opabex3rd  7782  opabex3  7783  op1stg  7816  op2ndg  7817  el2xptp  7850  dfoprab4f  7869  frxp  7938  opeliunxp2f  7997  tfrlem11  8190  omeu  8378  oeeui  8395  elixpsn  8683  fundmen  8775  xpsnen  8796  xpassen  8806  xpf1o  8875  unxpdomlem1  8956  djur  9608  dfac5lem1  9810  dfac5lem4  9813  axdc4lem  10142  nqereu  10616  mulcanenq  10647  archnq  10667  prlem934  10720  supsrlem  10798  supsr  10799  swrdccatin1  14366  swrdccat3blem  14380  fsum2dlem  15410  fprod2dlem  15618  vdwlem10  16619  imasaddfnlem  17156  catideu  17301  iscatd2  17307  catlid  17309  catpropd  17335  symg2bas  18915  efgmval  19233  efgi  19240  vrgpval  19288  gsumcom2  19491  txkgen  22711  cnmpt21  22730  xkoinjcn  22746  txconn  22748  pt1hmeo  22865  cnextfvval  23124  qustgplem  23180  dvbsss  24971  axlowdim2  27231  axlowdim  27232  axcontlem10  27244  axcontlem12  27246  isnvlem  28873  br8d  30851  2ndresdju  30887  cnvoprabOLD  30957  gsumhashmul  31218  prsrn  31767  esum2dlem  31960  eulerpartlemgvv  32243  fineqvrep  32964  satf0op  33239  satffunlem1lem1  33264  satffunlem2lem1  33266  sategoelfvb  33281  elxpxp  33586  br8  33629  br6  33630  br4  33631  eldm3  33634  dfdm5  33653  frxp2  33718  xpord2pred  33719  frxp3  33724  xpord3pred  33725  elfuns  34144  brimg  34166  brapply  34167  brsuccf  34170  brrestrict  34178  dfrdg4  34180  cgrdegen  34233  brofs  34234  cgrextend  34237  brifs  34272  ifscgr  34273  brcgr3  34275  brcolinear2  34287  colineardim1  34290  brfs  34308  idinside  34313  btwnconn1lem7  34322  btwnconn1lem11  34326  btwnconn1lem12  34327  brsegle  34337  outsideofeu  34360  fvray  34370  linedegen  34372  fvline  34373  bj-inftyexpiinv  35306  bj-inftyexpidisj  35308  finxpeq2  35485  finxpreclem6  35494  finxpsuclem  35495  curfv  35684  isdivrngo  36035  drngoi  36036  dicelval3  39121  dihjatcclem4  39362  dropab1  41954  relopabVD  42410  funressndmafv2rn  44602  dfatdmfcoafv2  44633  ichnreuop  44812  ichreuopeq  44813  reuopreuprim  44866  isthincd2lem2  46205