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 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1568  {cpr 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-v 3464  df-un 3918  df-sn 4595  df-pr 4597

This theorem is referenced by:  opeq2  4844  opthwiener  5501  fprg  7156  fprb  7196  fnprb  7210  fnpr2g  7212  opthreg  9590  fzosplitprm1  13810  s2prop  14947  chnccat  18685  gsumprval  18749  indislem  23140  isconn  23553  hmphindis  23937  wilthlem2  27213  ispth  30040  wwlksnredwwlkn  30214  wwlksnextfun  30217  wwlksnextinj  30218  wwlksnextsurj  30219  wwlksnextbij  30221  clwlkclwwlklem2a1  30313  clwlkclwwlklem2a4  30318  clwlkclwwlklem2  30321  clwwisshclwwslemlem  30334  clwwlkn2  30365  clwwlkf  30368  clwwlknonex2lem1  30428  eupth2lem3lem3  30551  eupth2  30560  frcond1  30587  nfrgr2v  30593  frgr3v  30596  n4cyclfrgr  30612  measxun2  34570  altopthsn  36411  mapdindp4  42447  clnbgrgrimlem  48647  gpgov  48756  gpgprismgriedgdmss  48766  gpgedg2ov  48780  gpgedg2iv  48781  gpg3kgrtriexlem6  48802  gpgprismgr4cycllem3  48811  grlimedgnedg  48845  2arymaptf1  49382  rrx2xpref1o  49447