Theorem preq1d 4692

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

Syntax hints:   → wi 4   = wceq 1541  {cpr 4578

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-sn 4577  df-pr 4579

This theorem is referenced by:  propeqop  5447  opthwiener  5454  fprg  7088  fprb  7128  fnpr2g  7144  dif1en  9071  dfac2b  10019  symg2bas  19303  crctcshwlkn0lem6  29791  wwlksnredwwlkn  29871  wwlksnextprop  29888  clwwlk1loop  29963  clwlkclwwlklem2fv1  29970  clwlkclwwlklem2fv2  29971  clwlkclwwlklem2a  29973  clwlkclwwlklem3  29976  clwwisshclwwslem  29989  clwwlknlbonbgr1  30014  clwwlkn1  30016  frcond1  30241  frgr1v  30246  nfrgr2v  30247  frgr3v  30250  n4cyclfrgr  30266  2clwwlk2clwwlklem  30321  wopprc  43062  mnurndlem1  44313  grtriclwlk3  47975  isubgr3stgrlem4  47999  gpgedgiov  48095  gpgedg2ov  48096  gpgedg2iv  48097  pgnbgreunbgrlem5lem1  48150  pgnbgreunbgrlem5lem2  48151  pgnbgreunbgrlem5lem3  48152  grlimedgnedg  48161  2arymaptf1  48684  rrx2xpref1o  48749