Theorem opeq1 4805

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 2826	. . . 4 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V))
2	1	anbi1d 630	. . 3 ⊢ (𝐴 = 𝐵 → ((𝐴 ∈ V ∧ 𝐶 ∈ V) ↔ (𝐵 ∈ V ∧ 𝐶 ∈ V)))
3		sneq 4572	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵})
4		preq1 4670	. . . 4 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
5	3, 4	preq12d 4678	. . 3 ⊢ (𝐴 = 𝐵 → {{𝐴}, {𝐴, 𝐶}} = {{𝐵}, {𝐵, 𝐶}})
6	2, 5	ifbieq1d 4484	. 2 ⊢ (𝐴 = 𝐵 → if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅) = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅))
7		dfopif 4801	. 2 ⊢ ⟨𝐴, 𝐶⟩ = if((𝐴 ∈ V ∧ 𝐶 ∈ V), {{𝐴}, {𝐴, 𝐶}}, ∅)
8		dfopif 4801	. 2 ⊢ ⟨𝐵, 𝐶⟩ = if((𝐵 ∈ V ∧ 𝐶 ∈ V), {{𝐵}, {𝐵, 𝐶}}, ∅)
9	6, 7, 8	3eqtr4g 2803	1 ⊢ (𝐴 = 𝐵 → ⟨𝐴, 𝐶⟩ = ⟨𝐵, 𝐶⟩)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2106  Vcvv 3430  ∅c0 4257  ifcif 4460  {csn 4562  {cpr 4564  ⟨cop 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3432  df-dif 3890  df-un 3892  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569

This theorem is referenced by:  opeq12  4807  opeq1i  4808  opeq1d  4811  oteq1  4814  breq1  5077  cbvopab1  5149  cbvopab1g  5150  cbvopab1s  5152  cbvopab1v  5153  opthg  5391  eqvinop  5400  sbcop1  5401  opelopabsb  5441  opelxp  5621  elvvv  5658  opabid2  5732  opeliunxp2  5741  elsnres  5925  elimasngOLD  5992  dmsnopg  6110  reuop  6190  funopg  6461  f1osng  6750  f1oprswap  6753  dmfco  6857  fvelrn  6947  fsng  7002  funsneqopb  7017  fprg  7020  fvrnressn  7026  funfvima3  7105  oveq1  7275  oprabidw  7299  oprabid  7300  dfoprab2  7324  cbvoprab1  7353  elxp4  7760  elxp5  7761  opabex3d  7798  opabex3rd  7799  opabex3  7800  op1stg  7833  op2ndg  7834  el2xptp  7867  dfoprab4f  7886  frxp  7955  opeliunxp2f  8014  tfrlem11  8207  omeu  8404  oeeui  8421  elixpsn  8713  fundmen  8809  xpsnen  8830  xpassen  8841  xpf1o  8914  unxpdomlem1  9015  djur  9665  dfac5lem1  9867  dfac5lem4  9870  axdc4lem  10199  nqereu  10673  mulcanenq  10704  archnq  10724  prlem934  10777  supsrlem  10855  supsr  10856  swrdccatin1  14426  swrdccat3blem  14440  fsum2dlem  15470  fprod2dlem  15678  vdwlem10  16679  imasaddfnlem  17227  catideu  17372  iscatd2  17378  catlid  17380  catpropd  17406  symg2bas  18988  efgmval  19306  efgi  19313  vrgpval  19361  gsumcom2  19564  txkgen  22791  cnmpt21  22810  xkoinjcn  22826  txconn  22828  pt1hmeo  22945  cnextfvval  23204  qustgplem  23260  dvbsss  25054  axlowdim2  27316  axlowdim  27317  axcontlem10  27329  axcontlem12  27331  isnvlem  28958  br8d  30936  2ndresdju  30972  cnvoprabOLD  31041  gsumhashmul  31302  prsrn  31851  esum2dlem  32046  eulerpartlemgvv  32329  fineqvrep  33050  satf0op  33325  satffunlem1lem1  33350  satffunlem2lem1  33352  sategoelfvb  33367  elxpxp  33669  br8  33709  br6  33710  br4  33711  eldm3  33714  dfdm5  33733  frxp2  33777  xpord2pred  33778  frxp3  33783  xpord3pred  33784  elfuns  34203  brimg  34225  brapply  34226  brsuccf  34229  brrestrict  34237  dfrdg4  34239  cgrdegen  34292  brofs  34293  cgrextend  34296  brifs  34331  ifscgr  34332  brcgr3  34334  brcolinear2  34346  colineardim1  34349  brfs  34367  idinside  34372  btwnconn1lem7  34381  btwnconn1lem11  34385  btwnconn1lem12  34386  brsegle  34396  outsideofeu  34419  fvray  34429  linedegen  34431  fvline  34432  bj-inftyexpiinv  35365  bj-inftyexpidisj  35367  finxpeq2  35544  finxpreclem6  35553  finxpsuclem  35554  curfv  35743  isdivrngo  36094  drngoi  36095  dicelval3  39180  dihjatcclem4  39421  dropab1  42024  relopabVD  42480  funressndmafv2rn  44671  dfatdmfcoafv2  44702  ichnreuop  44880  ichreuopeq  44881  reuopreuprim  44934  isthincd2lem2  46273