Theorem opeq1 4829

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 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4590	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4690	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4698	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4504	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4826	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4826	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  Vcvv 3440  ∅c0 4285  ifcif 4479  {csn 4580  {cpr 4582  ⟨cop 4586

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587

This theorem is referenced by:  opeq12  4831  opeq1i  4832  opeq1d  4835  oteq1  4838  breq1  5101  cbvopab1  5172  cbvopab1g  5173  cbvopab1s  5175  cbvopab1v  5176  opthg  5425  eqvinop  5435  sbcop1  5436  opelopabsb  5478  opelxp  5660  elvvv  5700  opabid2  5777  opeliunxp2  5787  elsnres  5980  dmsnopg  6171  reuop  6251  funopg  6526  f1osng  6816  f1oprswap  6819  dmfco  6930  fvelrn  7021  fsng  7082  funsneqopb  7097  fprg  7100  fvrnressn  7106  funfvima3  7182  oveq1  7365  oprabidw  7389  oprabid  7390  dfoprab2  7416  cbvoprab1  7445  elxp4  7864  elxp5  7865  opabex3d  7909  opabex3rd  7910  opabex3  7911  op1stg  7945  op2ndg  7946  el2xptp  7979  dfoprab4f  8000  frxp  8068  frxp2  8086  xpord2pred  8087  opeliunxp2f  8152  tfrlem11  8319  omeu  8512  oeeui  8530  elixpsn  8875  fundmen  8968  xpsnen  8989  xpassen  8999  xpf1o  9067  unxpdomlem1  9156  djur  9831  dfac5lem1  10033  dfac5lem4  10036  dfac5lem4OLD  10038  axdc4lem  10365  nqereu  10840  mulcanenq  10871  archnq  10891  prlem934  10944  supsrlem  11022  supsr  11023  swrdccatin1  14648  swrdccat3blem  14662  fsum2dlem  15693  fprod2dlem  15903  vdwlem10  16918  imasaddfnlem  17449  catideu  17598  iscatd2  17604  catlid  17606  catpropd  17632  symg2bas  19322  efgmval  19641  efgi  19648  vrgpval  19696  gsumcom2  19904  rngqiprngimfo  21256  pzriprnglem10  21445  pzriprnglem11  21446  txkgen  23596  cnmpt21  23615  xkoinjcn  23631  txconn  23633  pt1hmeo  23750  cnextfvval  24009  qustgplem  24065  dvbsss  25859  axlowdim2  29033  axlowdim  29034  axcontlem10  29046  axcontlem12  29048  isnvlem  30685  br8d  32686  2ndresdju  32727  gsumhashmul  33150  gsumwrd2dccatlem  33159  rlocf1  33355  idomsubr  33391  prsrn  34072  esum2dlem  34249  eulerpartlemgvv  34533  fineqvrep  35270  satf0op  35571  satffunlem1lem1  35596  satffunlem2lem1  35598  sategoelfvb  35613  br8  35950  br6  35951  br4  35952  eldm3  35955  dfdm5  35967  elfuns  36107  brimg  36129  brapply  36130  lemsuccf  36133  brrestrict  36143  dfrdg4  36145  cgrdegen  36198  brofs  36199  cgrextend  36202  brifs  36237  ifscgr  36238  brcgr3  36240  brcolinear2  36252  colineardim1  36255  brfs  36273  idinside  36278  btwnconn1lem7  36287  btwnconn1lem11  36291  btwnconn1lem12  36292  brsegle  36302  outsideofeu  36325  fvray  36335  linedegen  36337  fvline  36338  cbvoprab1vw  36431  cbvoprab13vw  36435  cbvopab1davw  36458  cbvoprab1davw  36465  bj-inftyexpiinv  37413  bj-inftyexpidisj  37415  finxpeq2  37592  finxpreclem6  37601  finxpsuclem  37602  curfv  37801  isdivrngo  38151  drngoi  38152  dicelval3  41440  dihjatcclem4  41681  dropab1  44687  relopabVD  45141  funressndmafv2rn  47469  dfatdmfcoafv2  47500  ichnreuop  47718  ichreuopeq  47719  reuopreuprim  47772  gpgedgvtx0  48307  gpgedgvtx1  48308  gpgcubic  48325  gpg5nbgr3star  48327  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem6  48370  pgnbgreunbgr  48371  sectpropdlem  49281  ssccatid  49317  upfval2  49422  isthincd2lem2  49680