Theorem preq2d 4679

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

Syntax hints:   → wi 4   = wceq 1547  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  opeq2  4812  opthwiener  5462  fprg  7105  fprb  7145  fnprb  7159  fnpr2g  7161  opthreg  9537  fzosplitprm1  13731  s2prop  14867  chnccat  18590  gsumprval  18654  indislem  22990  isconn  23403  hmphindis  23787  wilthlem2  27057  ispth  29814  wwlksnredwwlkn  29988  wwlksnextfun  29991  wwlksnextinj  29992  wwlksnextsurj  29993  wwlksnextbij  29995  clwlkclwwlklem2a1  30087  clwlkclwwlklem2a4  30092  clwlkclwwlklem2  30095  clwwisshclwwslemlem  30108  clwwlkn2  30139  clwwlkf  30142  clwwlknonex2lem1  30202  eupth2lem3lem3  30325  eupth2  30334  frcond1  30361  nfrgr2v  30367  frgr3v  30370  n4cyclfrgr  30386  measxun2  34401  altopthsn  36196  mapdindp4  42222  clnbgrgrimlem  48431  gpgov  48540  gpgprismgriedgdmss  48550  gpgedg2ov  48564  gpgedg2iv  48565  gpg3kgrtriexlem6  48586  gpgprismgr4cycllem3  48595  grlimedgnedg  48629  2arymaptf1  49151  rrx2xpref1o  49216