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

Theorem preq2d 4247
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 4241 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2syl 17 1 (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  {cpr 4152
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-un 3561  df-sn 4151  df-pr 4153
This theorem is referenced by:  opeq2  4373  opthwiener  4938  fprg  6379  fnprb  6429  fnpr2g  6431  opthreg  8462  s2prop  13591  gsumprval  17205  indislem  20717  isconn  21129  hmphindis  21513  wilthlem2  24702  ispth  26495  wwlksnredwwlkn  26666  wwlksnextfun  26669  wwlksnextinj  26670  wwlksnextsur  26671  wwlksnextbij  26673  clwlkclwwlklem2a1  26767  clwlkclwwlklem2a4  26772  clwlkclwwlklem2  26775  clwwlksn2  26783  clwwlksf  26788  clwwisshclwwslemlem  26799  eupth2lem3lem3  26963  eupth2  26972  frcond1  27003  nfrgr2v  27007  frgr3v  27010  n4cyclfrgr  27026  extwwlkfablem1  27073  measxun2  30066  fprb  31394  altopthsn  31731  mapdindp4  36513
  Copyright terms: Public domain W3C validator