Theorem opeq1 4831

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 2825	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 632	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4592	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4692	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4700	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4506	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4828	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4828	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ∅c0 4287  ifcif 4481  {csn 4582  {cpr 4584  ⟨cop 4588

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  opeq12  4833  opeq1i  4834  opeq1d  4837  oteq1  4840  breq1  5103  cbvopab1  5174  cbvopab1g  5175  cbvopab1s  5177  cbvopab1v  5178  opthg  5433  eqvinop  5443  sbcop1  5444  opelopabsb  5486  opelxp  5668  elvvv  5708  opabid2  5785  opeliunxp2  5795  elsnres  5988  dmsnopg  6179  reuop  6259  funopg  6534  f1osng  6824  f1oprswap  6827  dmfco  6938  fvelrn  7030  fsng  7092  funsneqopb  7107  fprg  7110  fvrnressn  7116  funfvima3  7192  oveq1  7375  oprabidw  7399  oprabid  7400  dfoprab2  7426  cbvoprab1  7455  elxp4  7874  elxp5  7875  opabex3d  7919  opabex3rd  7920  opabex3  7921  op1stg  7955  op2ndg  7956  el2xptp  7989  dfoprab4f  8010  frxp  8078  frxp2  8096  xpord2pred  8097  opeliunxp2f  8162  tfrlem11  8329  omeu  8522  oeeui  8540  elixpsn  8887  fundmen  8980  xpsnen  9001  xpassen  9011  xpf1o  9079  unxpdomlem1  9168  djur  9843  dfac5lem1  10045  dfac5lem4  10048  dfac5lem4OLD  10050  axdc4lem  10377  nqereu  10852  mulcanenq  10883  archnq  10903  prlem934  10956  supsrlem  11034  supsr  11035  swrdccatin1  14660  swrdccat3blem  14674  fsum2dlem  15705  fprod2dlem  15915  vdwlem10  16930  imasaddfnlem  17461  catideu  17610  iscatd2  17616  catlid  17618  catpropd  17644  symg2bas  19334  efgmval  19653  efgi  19660  vrgpval  19708  gsumcom2  19916  rngqiprngimfo  21268  pzriprnglem10  21457  pzriprnglem11  21458  txkgen  23608  cnmpt21  23627  xkoinjcn  23643  txconn  23645  pt1hmeo  23762  cnextfvval  24021  qustgplem  24077  dvbsss  25871  axlowdim2  29045  axlowdim  29046  axcontlem10  29058  axcontlem12  29060  isnvlem  30697  br8d  32697  2ndresdju  32738  gsumhashmul  33160  gsumwrd2dccatlem  33170  rlocf1  33366  idomsubr  33402  prsrn  34092  esum2dlem  34269  eulerpartlemgvv  34553  fineqvrep  35289  satf0op  35590  satffunlem1lem1  35615  satffunlem2lem1  35617  sategoelfvb  35632  br8  35969  br6  35970  br4  35971  eldm3  35974  dfdm5  35986  elfuns  36126  brimg  36148  brapply  36149  lemsuccf  36152  brrestrict  36162  dfrdg4  36164  cgrdegen  36217  brofs  36218  cgrextend  36221  brifs  36256  ifscgr  36257  brcgr3  36259  brcolinear2  36271  colineardim1  36274  brfs  36292  idinside  36297  btwnconn1lem7  36306  btwnconn1lem11  36310  btwnconn1lem12  36311  brsegle  36321  outsideofeu  36344  fvray  36354  linedegen  36356  fvline  36357  cbvoprab1vw  36450  cbvoprab13vw  36454  cbvopab1davw  36477  cbvoprab1davw  36484  bj-inftyexpiinv  37460  bj-inftyexpidisj  37462  finxpeq2  37639  finxpreclem6  37648  finxpsuclem  37649  curfv  37848  isdivrngo  38198  drngoi  38199  dicelval3  41553  dihjatcclem4  41794  dropab1  44799  relopabVD  45253  funressndmafv2rn  47580  dfatdmfcoafv2  47611  ichnreuop  47829  ichreuopeq  47830  reuopreuprim  47883  gpgedgvtx0  48418  gpgedgvtx1  48419  gpgcubic  48436  gpg5nbgr3star  48438  pgnbgreunbgrlem3  48475  pgnbgreunbgrlem6  48481  pgnbgreunbgr  48482  sectpropdlem  49392  ssccatid  49428  upfval2  49533  isthincd2lem2  49791