Theorem opeq1 4827

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 2816	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 631	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4589	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4687	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4695	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4503	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4824	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4824	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  Vcvv 3438  ∅c0 4286  ifcif 4478  {csn 4579  {cpr 4581  ⟨cop 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  opeq12  4829  opeq1i  4830  opeq1d  4833  oteq1  4836  breq1  5098  cbvopab1  5169  cbvopab1g  5170  cbvopab1s  5172  cbvopab1v  5173  opthg  5424  eqvinop  5434  sbcop1  5435  opelopabsb  5477  opelxp  5659  elvvv  5699  opabid2  5775  opeliunxp2  5785  elsnres  5976  dmsnopg  6166  reuop  6245  funopg  6520  f1osng  6809  f1oprswap  6812  dmfco  6923  fvelrn  7014  fsng  7075  funsneqopb  7090  fprg  7093  fvrnressn  7099  funfvima3  7176  oveq1  7360  oprabidw  7384  oprabid  7385  dfoprab2  7411  cbvoprab1  7440  elxp4  7862  elxp5  7863  opabex3d  7907  opabex3rd  7908  opabex3  7909  op1stg  7943  op2ndg  7944  el2xptp  7977  dfoprab4f  7998  frxp  8066  frxp2  8084  xpord2pred  8085  opeliunxp2f  8150  tfrlem11  8317  omeu  8510  oeeui  8527  elixpsn  8871  fundmen  8963  xpsnen  8985  xpassen  8995  xpf1o  9063  unxpdomlem1  9155  djur  9834  dfac5lem1  10036  dfac5lem4  10039  dfac5lem4OLD  10041  axdc4lem  10368  nqereu  10842  mulcanenq  10873  archnq  10893  prlem934  10946  supsrlem  11024  supsr  11025  swrdccatin1  14649  swrdccat3blem  14663  fsum2dlem  15695  fprod2dlem  15905  vdwlem10  16920  imasaddfnlem  17450  catideu  17599  iscatd2  17605  catlid  17607  catpropd  17633  symg2bas  19290  efgmval  19609  efgi  19616  vrgpval  19664  gsumcom2  19872  rngqiprngimfo  21226  pzriprnglem10  21415  pzriprnglem11  21416  txkgen  23555  cnmpt21  23574  xkoinjcn  23590  txconn  23592  pt1hmeo  23709  cnextfvval  23968  qustgplem  24024  dvbsss  25819  axlowdim2  28923  axlowdim  28924  axcontlem10  28936  axcontlem12  28938  isnvlem  30572  br8d  32571  2ndresdju  32606  gsumhashmul  33027  gsumwrd2dccatlem  33032  rlocf1  33226  idomsubr  33261  prsrn  33884  esum2dlem  34061  eulerpartlemgvv  34346  fineqvrep  35072  satf0op  35352  satffunlem1lem1  35377  satffunlem2lem1  35379  sategoelfvb  35394  br8  35731  br6  35732  br4  35733  eldm3  35736  dfdm5  35748  elfuns  35891  brimg  35913  brapply  35914  brsuccf  35917  brrestrict  35925  dfrdg4  35927  cgrdegen  35980  brofs  35981  cgrextend  35984  brifs  36019  ifscgr  36020  brcgr3  36022  brcolinear2  36034  colineardim1  36037  brfs  36055  idinside  36060  btwnconn1lem7  36069  btwnconn1lem11  36073  btwnconn1lem12  36074  brsegle  36084  outsideofeu  36107  fvray  36117  linedegen  36119  fvline  36120  cbvoprab1vw  36213  cbvoprab13vw  36217  cbvopab1davw  36240  cbvoprab1davw  36247  bj-inftyexpiinv  37184  bj-inftyexpidisj  37186  finxpeq2  37363  finxpreclem6  37372  finxpsuclem  37373  curfv  37582  isdivrngo  37932  drngoi  37933  dicelval3  41162  dihjatcclem4  41403  dropab1  44423  relopabVD  44877  funressndmafv2rn  47211  dfatdmfcoafv2  47242  ichnreuop  47460  ichreuopeq  47461  reuopreuprim  47514  gpgedgvtx0  48049  gpgedgvtx1  48050  gpgcubic  48067  gpg5nbgr3star  48069  pgnbgreunbgrlem3  48106  pgnbgreunbgrlem6  48112  pgnbgreunbgr  48113  sectpropdlem  49025  ssccatid  49061  upfval2  49166  isthincd2lem2  49424