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

Theorem preq1d 4705
Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)
Hypothesis
Ref Expression
preq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
preq1d (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})

Proof of Theorem preq1d
StepHypRef Expression
1 preq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 preq1 4699 . 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:  propeqop  5469  opthwiener  5476  fprg  7106  fprb  7148  fnpr2g  7165  dif1en  9111  dif1enOLD  9113  dfac2b  10073  symg2bas  19181  crctcshwlkn0lem6  28802  wwlksnredwwlkn  28882  wwlksnextprop  28899  clwwlk1loop  28974  clwlkclwwlklem2fv1  28981  clwlkclwwlklem2fv2  28982  clwlkclwwlklem2a  28984  clwlkclwwlklem3  28987  clwwisshclwwslem  29000  clwwlknlbonbgr1  29025  clwwlkn1  29027  frcond1  29252  frgr1v  29257  nfrgr2v  29258  frgr3v  29261  n4cyclfrgr  29277  2clwwlk2clwwlklem  29332  wopprc  41383  mnurndlem1  42635  isomuspgrlem2d  46097  2arymaptf1  46813  rrx2xpref1o  46878
  Copyright terms: Public domain W3C validator