Theorem preq1d 4630

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

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		preq1 4624	. 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1542  {cpr 4518

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-un 3848  df-sn 4517  df-pr 4519

This theorem is referenced by:  propeqop  5364  opthwiener  5371  fprg  6927  fprb  6966  fnpr2g  6983  dif1en  8761  dfac2b  9630  symg2bas  18639  crctcshwlkn0lem6  27753  wwlksnredwwlkn  27833  wwlksnextprop  27850  clwwlk1loop  27925  clwlkclwwlklem2fv1  27932  clwlkclwwlklem2fv2  27933  clwlkclwwlklem2a  27935  clwlkclwwlklem3  27938  clwwisshclwwslem  27951  clwwlknlbonbgr1  27976  clwwlkn1  27978  frcond1  28203  frgr1v  28208  nfrgr2v  28209  frgr3v  28212  n4cyclfrgr  28228  2clwwlk2clwwlklem  28283  wopprc  40444  mnurndlem1  41461  isomuspgrlem2d  44837  2arymaptf1  45553  rrx2xpref1o  45618