Theorem preq1d 4764

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 4758	. 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴, 𝐶} = {𝐵, 𝐶})

Syntax hints:   → wi 4   = wceq 1537  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  propeqop  5526  opthwiener  5533  fprg  7189  fprb  7231  fnpr2g  7247  dif1en  9226  dif1enOLD  9228  dfac2b  10200  symg2bas  19434  crctcshwlkn0lem6  29848  wwlksnredwwlkn  29928  wwlksnextprop  29945  clwwlk1loop  30020  clwlkclwwlklem2fv1  30027  clwlkclwwlklem2fv2  30028  clwlkclwwlklem2a  30030  clwlkclwwlklem3  30033  clwwisshclwwslem  30046  clwwlknlbonbgr1  30071  clwwlkn1  30073  frcond1  30298  frgr1v  30303  nfrgr2v  30304  frgr3v  30307  n4cyclfrgr  30323  2clwwlk2clwwlklem  30378  wopprc  42987  mnurndlem1  44250  grtriclwlk3  47796  2arymaptf1  48387  rrx2xpref1o  48452