Theorem preq2d 4697

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  opeq2  4840  opthwiener  5486  fprg  7160  fprb  7200  fnprb  7215  fnpr2g  7217  opthreg  9623  fzosplitprm1  13917  s2prop  15064  chnccat  18806  gsumprval  18883  indislem  23324  isconn  23737  hmphindis  24122  wilthlem2  27402  ispth  30312  wwlksnredwwlkn  30490  wwlksnextfun  30493  wwlksnextinj  30494  wwlksnextsurj  30495  wwlksnextbij  30497  clwlkclwwlklem2a1  30589  clwlkclwwlklem2a4  30594  clwlkclwwlklem2  30597  clwwisshclwwslemlem  30610  clwwlkn2  30641  clwwlkf  30644  clwwlknonex2lem1  30704  eupth2lem3lem3  30837  eupth2  30846  frcond1  30873  nfrgr2v  30879  frgr3v  30882  n4cyclfrgr  30898  measxun2  34890  altopthsn  36819  mapdindp4  42874  clnbgrgrimlem  49125  gpgov  49234  gpgprismgriedgdmss  49244  gpgedg2ov  49258  gpgedg2iv  49259  gpg3kgrtriexlem6  49280  gpgprismgr4cycllem3  49289  grlimedgnedg  49323  2arymaptf1  49859