Theorem preq1d 4696

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

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

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  propeqop  5455  opthwiener  5462  fprg  7100  fprb  7140  fnpr2g  7156  dif1en  9086  dfac2b  10041  symg2bas  19322  crctcshwlkn0lem6  29888  wwlksnredwwlkn  29968  wwlksnextprop  29985  clwwlk1loop  30063  clwlkclwwlklem2fv1  30070  clwlkclwwlklem2fv2  30071  clwlkclwwlklem2a  30073  clwlkclwwlklem3  30076  clwwisshclwwslem  30089  clwwlknlbonbgr1  30114  clwwlkn1  30116  frcond1  30341  frgr1v  30346  nfrgr2v  30347  frgr3v  30350  n4cyclfrgr  30366  2clwwlk2clwwlklem  30421  wopprc  43268  mnurndlem1  44518  grtriclwlk3  48187  isubgr3stgrlem4  48211  gpgedgiov  48307  gpgedg2ov  48308  gpgedg2iv  48309  pgnbgreunbgrlem5lem1  48362  pgnbgreunbgrlem5lem2  48363  pgnbgreunbgrlem5lem3  48364  grlimedgnedg  48373  2arymaptf1  48895  rrx2xpref1o  48960