Theorem preq2d 4636

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

Hypothesis

Ref	Expression
preq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
preq2d	⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Proof of Theorem preq2d

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		preq2 4630	. 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1538  {cpr 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  opeq2  4765  opeq2OLD  4766  opthwiener  5369  fprg  6894  fprb  6933  fnprb  6948  fnpr2g  6950  opthreg  9065  fzosplitprm1  13142  s2prop  14260  gsumprval  17890  indislem  21605  isconn  22018  hmphindis  22402  wilthlem2  25654  ispth  27512  wwlksnredwwlkn  27681  wwlksnextfun  27684  wwlksnextinj  27685  wwlksnextsurj  27686  wwlksnextbij  27688  clwlkclwwlklem2a1  27777  clwlkclwwlklem2a4  27782  clwlkclwwlklem2  27785  clwwisshclwwslemlem  27798  clwwlkn2  27829  clwwlkf  27832  clwwlknonex2lem1  27892  eupth2lem3lem3  28015  eupth2  28024  frcond1  28051  nfrgr2v  28057  frgr3v  28060  n4cyclfrgr  28076  measxun2  31579  altopthsn  33535  mapdindp4  39019  isomuspgrlem2d  44349  2arymaptf1  45067  rrx2xpref1o  45132