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

Theorem preq2d 4675
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 4669 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2syl 17 1 (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  {cpr 4566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-v 3502  df-un 3945  df-sn 4565  df-pr 4567
This theorem is referenced by:  opeq2  4803  opthwiener  5401  fprg  6913  fprb  6952  fnprb  6966  fnpr2g  6968  opthreg  9070  fzosplitprm1  13137  s2prop  14259  gsumprval  17887  indislem  21524  isconn  21937  hmphindis  22321  wilthlem2  25560  ispth  27418  wwlksnredwwlkn  27587  wwlksnextfun  27590  wwlksnextinj  27591  wwlksnextsurj  27592  wwlksnextbij  27594  clwlkclwwlklem2a1  27684  clwlkclwwlklem2a4  27689  clwlkclwwlklem2  27692  clwwisshclwwslemlem  27705  clwwlkn2  27736  clwwlkf  27740  clwwlknonex2lem1  27800  eupth2lem3lem3  27923  eupth2  27932  frcond1  27959  nfrgr2v  27965  frgr3v  27968  n4cyclfrgr  27984  measxun2  31355  altopthsn  33306  mapdindp4  38726  isomuspgrlem2d  43828  rrx2xpref1o  44537
  Copyright terms: Public domain W3C validator