Theorem preq2d 4765

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 4759	. 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1537  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  opeq2  4898  opthwiener  5533  fprg  7189  fprb  7231  fnprb  7245  fnpr2g  7247  opthreg  9687  fzosplitprm1  13827  s2prop  14956  gsumprval  18726  indislem  23028  isconn  23442  hmphindis  23826  wilthlem2  27130  ispth  29759  wwlksnredwwlkn  29928  wwlksnextfun  29931  wwlksnextinj  29932  wwlksnextsurj  29933  wwlksnextbij  29935  clwlkclwwlklem2a1  30024  clwlkclwwlklem2a4  30029  clwlkclwwlklem2  30032  clwwisshclwwslemlem  30045  clwwlkn2  30076  clwwlkf  30079  clwwlknonex2lem1  30139  eupth2lem3lem3  30262  eupth2  30271  frcond1  30298  nfrgr2v  30304  frgr3v  30307  n4cyclfrgr  30323  measxun2  34174  altopthsn  35925  mapdindp4  41680  clnbgrgrimlem  47785  2arymaptf1  48387  rrx2xpref1o  48452