Theorem preq2d 4736

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

Syntax hints:   → wi 4   = wceq 1533  {cpr 4622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-un 3945  df-sn 4621  df-pr 4623

This theorem is referenced by:  opeq2  4866  opthwiener  5504  fprg  7145  fprb  7187  fnprb  7201  fnpr2g  7203  opthreg  9609  fzosplitprm1  13739  s2prop  14855  gsumprval  18611  indislem  22825  isconn  23239  hmphindis  23623  wilthlem2  26917  ispth  29449  wwlksnredwwlkn  29618  wwlksnextfun  29621  wwlksnextinj  29622  wwlksnextsurj  29623  wwlksnextbij  29625  clwlkclwwlklem2a1  29714  clwlkclwwlklem2a4  29719  clwlkclwwlklem2  29722  clwwisshclwwslemlem  29735  clwwlkn2  29766  clwwlkf  29769  clwwlknonex2lem1  29829  eupth2lem3lem3  29952  eupth2  29961  frcond1  29988  nfrgr2v  29994  frgr3v  29997  n4cyclfrgr  30013  measxun2  33697  altopthsn  35428  mapdindp4  41084  isomuspgrlem2d  46984  2arymaptf1  47527  rrx2xpref1o  47592