Theorem preq2d 4070

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 4064	. 2 |- ( A = B -> { C , A } = { C , B } )
3	1, 2	syl 16	1 |- ( ph -> { C , A } = { C , B } )

Syntax hints:   -> wi 4   = wceq 1370   {cpr 3988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-un 3442  df-sn 3987  df-pr 3989

This theorem is referenced by:  opeq2  4169  opthwiener  4702  fprg  6001  fnprb  6046  opthreg  7936  s2prop  12643  gsumprval  15634  indislem  18737  iscon  19150  hmphindis  19503  wilthlem2  22541  ispth  23620  1pthonlem2  23642  2pthoncl  23655  eupath2lem3  23753  eupath2  23754  measxun2  26770  fprb  27729  altopthsn  28137  wwlknredwwlkn  30507  wwlkextfun  30510  wwlkextinj  30511  wwlkextsur  30512  wwlkextbij  30514  clwwlkn2  30587  clwlkisclwwlklem2a1  30590  clwlkisclwwlklem2a4  30595  clwlkisclwwlklem1  30598  clwwlkf  30605  clwwisshclwwlem1  30618  frgraunss  30736  frgra2v  30740  frgra3v  30743  n4cyclfrgra  30759  extwwlkfablem1  30816  extwwlkfablem2  30820  mapdindp4  35707