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

Theorem preq2d 4706
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 4700 . 2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
31, 2syl 17 1 (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  {cpr 4593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920  df-sn 4592  df-pr 4594
This theorem is referenced by:  opeq2  4836  opthwiener  5476  fprg  7106  fprb  7148  fnprb  7163  fnpr2g  7165  opthreg  9561  fzosplitprm1  13689  s2prop  14803  gsumprval  18550  indislem  22366  isconn  22780  hmphindis  23164  wilthlem2  26434  ispth  28713  wwlksnredwwlkn  28882  wwlksnextfun  28885  wwlksnextinj  28886  wwlksnextsurj  28887  wwlksnextbij  28889  clwlkclwwlklem2a1  28978  clwlkclwwlklem2a4  28983  clwlkclwwlklem2  28986  clwwisshclwwslemlem  28999  clwwlkn2  29030  clwwlkf  29033  clwwlknonex2lem1  29093  eupth2lem3lem3  29216  eupth2  29225  frcond1  29252  nfrgr2v  29258  frgr3v  29261  n4cyclfrgr  29277  measxun2  32849  altopthsn  34575  mapdindp4  40215  isomuspgrlem2d  46097  2arymaptf1  46813  rrx2xpref1o  46878
  Copyright terms: Public domain W3C validator