Theorem preq2d 4701

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  opeq2  4844  opthwiener  5492  fprg  7186  fprb  7225  fnprb  7240  fnpr2g  7242  opthreg  9649  fzosplitprm1  13943  s2prop  15090  chnccat  18832  gsumprval  18909  indislem  23351  isconn  23764  hmphindis  24149  wilthlem2  27429  ispth  30339  wwlksnredwwlkn  30517  wwlksnextfun  30520  wwlksnextinj  30521  wwlksnextsurj  30522  wwlksnextbij  30524  clwlkclwwlklem2a1  30616  clwlkclwwlklem2a4  30621  clwlkclwwlklem2  30624  clwwisshclwwslemlem  30637  clwwlkn2  30668  clwwlkf  30671  clwwlknonex2lem1  30731  eupth2lem3lem3  30864  eupth2  30873  frcond1  30900  nfrgr2v  30906  frgr3v  30909  n4cyclfrgr  30925  measxun2  34926  altopthsn  36917  mapdindp4  42983  clnbgrgrimlem  49246  gpgov  49355  gpgprismgriedgdmss  49365  gpgedg2ov  49379  gpgedg2iv  49380  gpg3kgrtriexlem6  49401  gpgprismgr4cycllem3  49410  grlimedgnedg  49444  2arymaptf1  49980