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

Theorem preq2d 4307
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 4301 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2syl 17 1 (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  {cpr 4212
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-un 3612  df-sn 4211  df-pr 4213
This theorem is referenced by:  opeq2  4434  opthwiener  5005  fprg  6462  fnprb  6513  fnpr2g  6515  opthreg  8553  fzosplitprm1  12618  s2prop  13698  gsumprval  17328  indislem  20852  isconn  21264  hmphindis  21648  wilthlem2  24840  ispth  26675  wwlksnredwwlkn  26858  wwlksnextfun  26861  wwlksnextinj  26862  wwlksnextsur  26863  wwlksnextbij  26865  clwlkclwwlklem2a1  26958  clwlkclwwlklem2a4  26963  clwlkclwwlklem2  26966  clwwisshclwwslemlem  26970  clwwlkn2  27007  clwwlkf  27010  clwwlknonex2lem1  27082  eupth2lem3lem3  27208  eupth2  27217  frcond1  27246  nfrgr2v  27252  frgr3v  27255  n4cyclfrgr  27271  extwwlkfablem1OLD  27323  measxun2  30401  fprb  31795  altopthsn  32193  mapdindp4  37329
  Copyright terms: Public domain W3C validator