Theorem preq2d 4113

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

Syntax hints:   -> wi 4   = wceq 1379   {cpr 4029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030

This theorem is referenced by:  opeq2  4214  opthwiener  4749  fprg  6068  fnprb  6117  opthreg  8031  s2prop  12819  gsumprval  15824  indislem  19264  iscon  19677  hmphindis  20030  wilthlem2  23068  ispth  24243  1pthonlem2  24265  2pthoncl  24278  wwlknredwwlkn  24399  wwlkextfun  24402  wwlkextinj  24403  wwlkextsur  24404  wwlkextbij  24406  clwwlkn2  24448  clwlkisclwwlklem2a1  24452  clwlkisclwwlklem2a4  24457  clwlkisclwwlklem1  24460  clwwlkf  24467  clwwisshclwwlem1  24478  eupath2lem3  24652  eupath2  24653  frgraunss  24668  frgra2v  24672  frgra3v  24675  n4cyclfrgra  24691  extwwlkfablem1  24748  extwwlkfablem2  24752  measxun2  27818  fprb  28777  altopthsn  29185  mapdindp4  36520