MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  preq2d Structured version   Visualization version   GIF version

Theorem preq2d 4668
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
StepHypRef Expression
1 preq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 preq2 4662 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2syl 17 1 (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  {cpr 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-un 3938  df-sn 4558  df-pr 4560
This theorem is referenced by:  opeq2  4796  opthwiener  5395  fprg  6909  fprb  6948  fnprb  6962  fnpr2g  6964  opthreg  9069  fzosplitprm1  13135  s2prop  14257  gsumprval  17886  indislem  21536  isconn  21949  hmphindis  22333  wilthlem2  25573  ispth  27431  wwlksnredwwlkn  27600  wwlksnextfun  27603  wwlksnextinj  27604  wwlksnextsurj  27605  wwlksnextbij  27607  clwlkclwwlklem2a1  27697  clwlkclwwlklem2a4  27702  clwlkclwwlklem2  27705  clwwisshclwwslemlem  27718  clwwlkn2  27749  clwwlkf  27753  clwwlknonex2lem1  27813  eupth2lem3lem3  27936  eupth2  27945  frcond1  27972  nfrgr2v  27978  frgr3v  27981  n4cyclfrgr  27997  measxun2  31368  altopthsn  33319  mapdindp4  38739  isomuspgrlem2d  43873  rrx2xpref1o  44633
  Copyright terms: Public domain W3C validator