Theorem opeq1 4816

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 2824	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 632	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4577	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4677	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4685	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4491	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4813	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4813	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3429  ∅c0 4273  ifcif 4466  {csn 4567  {cpr 4569  ⟨cop 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  opeq12  4818  opeq1i  4819  opeq1d  4822  oteq1  4825  breq1  5088  cbvopab1  5159  cbvopab1g  5160  cbvopab1s  5162  cbvopab1v  5163  opthg  5430  eqvinop  5440  sbcop1  5441  opelopabsb  5485  opelxp  5667  elvvv  5707  opabid2  5784  opeliunxp2  5793  elsnres  5986  dmsnopg  6177  reuop  6257  funopg  6532  f1osng  6822  f1oprswap  6825  dmfco  6936  fvelrn  7028  fsng  7090  funsneqopb  7106  fprg  7109  fvrnressn  7115  funfvima3  7191  oveq1  7374  oprabidw  7398  oprabid  7399  dfoprab2  7425  cbvoprab1  7454  elxp4  7873  elxp5  7874  opabex3d  7918  opabex3rd  7919  opabex3  7920  op1stg  7954  op2ndg  7955  el2xptp  7988  dfoprab4f  8009  frxp  8076  frxp2  8094  xpord2pred  8095  opeliunxp2f  8160  tfrlem11  8327  omeu  8520  oeeui  8538  elixpsn  8885  fundmen  8978  xpsnen  8999  xpassen  9009  xpf1o  9077  unxpdomlem1  9166  djur  9843  dfac5lem1  10045  dfac5lem4  10048  dfac5lem4OLD  10050  axdc4lem  10377  nqereu  10852  mulcanenq  10883  archnq  10903  prlem934  10956  supsrlem  11034  supsr  11035  swrdccatin1  14687  swrdccat3blem  14701  fsum2dlem  15732  fprod2dlem  15945  vdwlem10  16961  imasaddfnlem  17492  catideu  17641  iscatd2  17647  catlid  17649  catpropd  17675  symg2bas  19368  efgmval  19687  efgi  19694  vrgpval  19742  gsumcom2  19950  rngqiprngimfo  21299  pzriprnglem10  21470  pzriprnglem11  21471  txkgen  23617  cnmpt21  23636  xkoinjcn  23652  txconn  23654  pt1hmeo  23771  cnextfvval  24030  qustgplem  24086  dvbsss  25869  axlowdim2  29029  axlowdim  29030  axcontlem10  29042  axcontlem12  29044  isnvlem  30681  br8d  32681  2ndresdju  32722  gsumhashmul  33128  gsumwrd2dccatlem  33138  rlocf1  33334  idomsubr  33370  prsrn  34059  esum2dlem  34236  eulerpartlemgvv  34520  fineqvrep  35258  satf0op  35559  satffunlem1lem1  35584  satffunlem2lem1  35586  sategoelfvb  35601  br8  35938  br6  35939  br4  35940  eldm3  35943  dfdm5  35955  elfuns  36095  brimg  36117  brapply  36118  lemsuccf  36121  brrestrict  36131  dfrdg4  36133  cgrdegen  36186  brofs  36187  cgrextend  36190  brifs  36225  ifscgr  36226  brcgr3  36228  brcolinear2  36240  colineardim1  36243  brfs  36261  idinside  36266  btwnconn1lem7  36275  btwnconn1lem11  36279  btwnconn1lem12  36280  brsegle  36290  outsideofeu  36313  fvray  36323  linedegen  36325  fvline  36326  cbvoprab1vw  36419  cbvoprab13vw  36423  cbvopab1davw  36446  cbvoprab1davw  36453  bj-inftyexpiinv  37522  bj-inftyexpidisj  37524  finxpeq2  37703  finxpreclem6  37712  finxpsuclem  37713  curfv  37921  isdivrngo  38271  drngoi  38272  dicelval3  41626  dihjatcclem4  41867  dropab1  44873  relopabVD  45327  funressndmafv2rn  47671  dfatdmfcoafv2  47702  ichnreuop  47932  ichreuopeq  47933  reuopreuprim  47986  gpgedgvtx0  48537  gpgedgvtx1  48538  gpgcubic  48555  gpg5nbgr3star  48557  pgnbgreunbgrlem3  48594  pgnbgreunbgrlem6  48600  pgnbgreunbgr  48601  sectpropdlem  49511  ssccatid  49547  upfval2  49652  isthincd2lem2  49910