Theorem preq2d 4275

Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Hypothesis

Ref	Expression
preq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
preq2d	|- ( ph -> { C , A } = { C , B } )

Proof of Theorem preq2d

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 |- ( ph -> A = B )
2		preq2 4269	. 2 |- ( A = B -> { C , A } = { C , B } )
3	1, 2	syl 17	1 |- ( ph -> { C , A } = { C , B } )

Syntax hints:   -> wi 4   = wceq 1483   {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  opeq2  4403  opthwiener  4976  fprg  6422  fnprb  6472  fnpr2g  6474  opthreg  8515  fzosplitprm1  12578  s2prop  13652  gsumprval  17281  indislem  20804  isconn  21216  hmphindis  21600  wilthlem2  24795  ispth  26619  wwlksnredwwlkn  26790  wwlksnextfun  26793  wwlksnextinj  26794  wwlksnextsur  26795  wwlksnextbij  26797  clwlkclwwlklem2a1  26893  clwlkclwwlklem2a4  26898  clwlkclwwlklem2  26901  clwwlksn2  26910  clwwlksf  26915  clwwisshclwwslemlem  26926  eupth2lem3lem3  27090  eupth2  27099  frcond1  27130  nfrgr2v  27136  frgr3v  27139  n4cyclfrgr  27155  extwwlkfablem1  27207  numclwwlkovf2exlem1  27211  measxun2  30273  fprb  31669  altopthsn  32068  mapdindp4  37012