Theorem preq2d 4118

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

Syntax hints:   -> wi 4   = wceq 1395   {cpr 4034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476  df-sn 4033  df-pr 4035

This theorem is referenced by:  opeq2  4220  opthwiener  4758  fprg  6081  fnprb  6131  opthreg  8052  s2prop  12873  gsumprval  16034  indislem  19627  iscon  20039  hmphindis  20423  wilthlem2  23468  ispth  24696  1pthonlem2  24718  2pthoncl  24731  wwlknredwwlkn  24852  wwlkextfun  24855  wwlkextinj  24856  wwlkextsur  24857  wwlkextbij  24859  clwwlkn2  24901  clwlkisclwwlklem2a1  24905  clwlkisclwwlklem2a4  24910  clwlkisclwwlklem1  24913  clwwlkf  24920  clwwisshclwwlem1  24931  eupath2lem3  25105  eupath2  25106  frgraunss  25121  frgra2v  25125  frgra3v  25128  n4cyclfrgra  25144  extwwlkfablem1  25200  extwwlkfablem2  25204  measxun2  28342  fprb  29377  altopthsn  29773  mapdindp4  37551