Theorem preq2d 4711

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cpr 4596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-un 3913  df-sn 4595  df-pr 4597

This theorem is used by:  opeq2  4844  opthwiener  5502  fprg  7159  fprb  7199  fnprb  7213  fnpr2g  7215  opthreg  9597  fzosplitprm1  13826  s2prop  14970  chnccat  18707  gsumprval  18775  indislem  23194  isconn  23607  hmphindis  23991  wilthlem2  27270  ispth  30107  wwlksnredwwlkn  30281  wwlksnextfun  30284  wwlksnextinj  30285  wwlksnextsurj  30286  wwlksnextbij  30288  clwlkclwwlklem2a1  30380  clwlkclwwlklem2a4  30385  clwlkclwwlklem2  30388  clwwisshclwwslemlem  30401  clwwlkn2  30432  clwwlkf  30435  clwwlknonex2lem1  30495  eupth2lem3lem3  30618  eupth2  30627  frcond1  30654  nfrgr2v  30660  frgr3v  30663  n4cyclfrgr  30679  measxun2  34632  altopthsn  36474  mapdindp4  42538  clnbgrgrimlem  48739  gpgov  48848  gpgprismgriedgdmss  48858  gpgedg2ov  48872  gpgedg2iv  48873  gpg3kgrtriexlem6  48894  gpgprismgr4cycllem3  48903  grlimedgnedg  48937  2arymaptf1  49474  rrx2xpref1o  49539