Theorem preq2d 4690

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

Syntax hints:   → wi 4   = wceq 1540  {cpr 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3435  df-un 3904  df-sn 4574  df-pr 4576

This theorem is referenced by:  opeq2  4823  opthwiener  5451  fprg  7082  fprb  7122  fnprb  7136  fnpr2g  7138  opthreg  9502  fzosplitprm1  13668  s2prop  14801  gsumprval  18549  indislem  22869  isconn  23282  hmphindis  23666  wilthlem2  26960  ispth  29653  wwlksnredwwlkn  29827  wwlksnextfun  29830  wwlksnextinj  29831  wwlksnextsurj  29832  wwlksnextbij  29834  clwlkclwwlklem2a1  29923  clwlkclwwlklem2a4  29928  clwlkclwwlklem2  29931  clwwisshclwwslemlem  29944  clwwlkn2  29975  clwwlkf  29978  clwwlknonex2lem1  30038  eupth2lem3lem3  30161  eupth2  30170  frcond1  30197  nfrgr2v  30203  frgr3v  30206  n4cyclfrgr  30222  measxun2  34191  altopthsn  35952  mapdindp4  41719  clnbgrgrimlem  47931  gpgov  48040  gpgprismgriedgdmss  48050  gpgedg2ov  48064  gpgedg2iv  48065  gpg3kgrtriexlem6  48086  gpgprismgr4cycllem3  48095  grlimedgnedg  48129  2arymaptf1  48652  rrx2xpref1o  48717