Theorem preq1d 4706

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

Syntax hints:   → wi 4   = wceq 1570  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  propeqop  5492  opthwiener  5499  fprg  7154  fprb  7194  fnpr2g  7210  dif1en  9147  dfac2b  10115  symg2bas  19464  crctcshwlkn0lem6  30145  wwlksnredwwlkn  30225  wwlksnextprop  30242  clwwlk1loop  30320  clwlkclwwlklem2fv1  30327  clwlkclwwlklem2fv2  30328  clwlkclwwlklem2a  30330  clwlkclwwlklem3  30333  clwwisshclwwslem  30346  clwwlknlbonbgr1  30371  clwwlkn1  30373  frcond1  30598  frgr1v  30603  nfrgr2v  30604  frgr3v  30607  n4cyclfrgr  30623  2clwwlk2clwwlklem  30678  wopprc  43740  mnurndlem1  44974  grtriclwlk3  48693  isubgr3stgrlem4  48717  gpgedgiov  48813  gpgedg2ov  48814  gpgedg2iv  48815  pgnbgreunbgrlem5lem1  48868  pgnbgreunbgrlem5lem2  48869  pgnbgreunbgrlem5lem3  48870  grlimedgnedg  48879  2arymaptf1  49416  rrx2xpref1o  49481