Theorem opeq1 4853

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 2821	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4616	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4713	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4721	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4530	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4850	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4850	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2794	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  Vcvv 3463  ∅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 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3420  df-v 3465  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  4855  opeq1i  4856  opeq1d  4859  oteq1  4862  breq1  5126  cbvopab1  5197  cbvopab1g  5198  cbvopab1s  5200  cbvopab1v  5201  opthg  5462  eqvinop  5472  sbcop1  5473  opelopabsb  5515  opelxp  5701  elvvv  5741  opabid2  5818  opeliunxp2  5829  elsnres  6019  dmsnopg  6213  reuop  6293  funopg  6580  f1osng  6869  f1oprswap  6872  dmfco  6985  fvelrn  7076  fsng  7137  funsneqopb  7152  fprg  7155  fvrnressn  7161  funfvima3  7238  oveq1  7420  oprabidw  7444  oprabid  7445  dfoprab2  7473  cbvoprab1  7502  elxp4  7926  elxp5  7927  opabex3d  7972  opabex3rd  7973  opabex3  7974  op1stg  8008  op2ndg  8009  el2xptp  8042  dfoprab4f  8063  frxp  8133  frxp2  8151  xpord2pred  8152  opeliunxp2f  8217  tfrlem11  8410  omeu  8605  oeeui  8622  elixpsn  8959  fundmen  9053  xpsnen  9077  xpassen  9088  xpf1o  9161  unxpdomlem1  9268  djur  9941  dfac5lem1  10145  dfac5lem4  10148  dfac5lem4OLD  10150  axdc4lem  10477  nqereu  10951  mulcanenq  10982  archnq  11002  prlem934  11055  supsrlem  11133  supsr  11134  swrdccatin1  14745  swrdccat3blem  14759  fsum2dlem  15788  fprod2dlem  15998  vdwlem10  17010  imasaddfnlem  17544  catideu  17689  iscatd2  17695  catlid  17697  catpropd  17723  symg2bas  19378  efgmval  19698  efgi  19705  vrgpval  19753  gsumcom2  19961  rngqiprngimfo  21273  pzriprnglem10  21463  pzriprnglem11  21464  txkgen  23606  cnmpt21  23625  xkoinjcn  23641  txconn  23643  pt1hmeo  23760  cnextfvval  24019  qustgplem  24075  dvbsss  25873  axlowdim2  28905  axlowdim  28906  axcontlem10  28918  axcontlem12  28920  isnvlem  30557  br8d  32557  2ndresdju  32594  gsumhashmul  33003  gsumwrd2dccatlem  33008  rlocf1  33216  idomsubr  33251  prsrn  33873  esum2dlem  34052  eulerpartlemgvv  34337  fineqvrep  35068  satf0op  35341  satffunlem1lem1  35366  satffunlem2lem1  35368  sategoelfvb  35383  br8  35715  br6  35716  br4  35717  eldm3  35720  dfdm5  35732  elfuns  35875  brimg  35897  brapply  35898  brsuccf  35901  brrestrict  35909  dfrdg4  35911  cgrdegen  35964  brofs  35965  cgrextend  35968  brifs  36003  ifscgr  36004  brcgr3  36006  brcolinear2  36018  colineardim1  36021  brfs  36039  idinside  36044  btwnconn1lem7  36053  btwnconn1lem11  36057  btwnconn1lem12  36058  brsegle  36068  outsideofeu  36091  fvray  36101  linedegen  36103  fvline  36104  cbvoprab1vw  36197  cbvoprab13vw  36201  cbvopab1davw  36224  cbvoprab1davw  36231  bj-inftyexpiinv  37168  bj-inftyexpidisj  37170  finxpeq2  37347  finxpreclem6  37356  finxpsuclem  37357  curfv  37566  isdivrngo  37916  drngoi  37917  dicelval3  41141  dihjatcclem4  41382  dropab1  44423  relopabVD  44878  funressndmafv2rn  47193  dfatdmfcoafv2  47224  ichnreuop  47417  ichreuopeq  47418  reuopreuprim  47471  gpgedgvtx0  47977  gpgedgvtx1  47978  gpgcubic  47993  gpg5nbgr3star  47995  upfval2  48905  isthincd2lem2  49062