Theorem preq1d 4700

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  propeqop  5484  opthwiener  5492  fprg  7186  fprb  7225  fnpr2g  7242  dif1en  9208  dfac2b  10239  symg2bas  19640  crctcshwlkn0lem6  30437  wwlksnredwwlkn  30517  wwlksnextprop  30534  clwwlk1loop  30612  clwlkclwwlklem2fv1  30619  clwlkclwwlklem2fv2  30620  clwlkclwwlklem2a  30622  clwlkclwwlklem3  30625  clwwisshclwwslem  30638  clwwlknlbonbgr1  30663  clwwlkn1  30665  frcond1  30900  frgr1v  30905  nfrgr2v  30906  frgr3v  30909  n4cyclfrgr  30925  2clwwlk2clwwlklem  30980  wopprc  44241  mnurndlem1  45468  grtriclwlk3  49258  isubgr3stgrlem4  49282  gpgedgiov  49378  gpgedg2ov  49379  gpgedg2iv  49380  pgnbgreunbgrlem5lem1  49433  pgnbgreunbgrlem5lem2  49434  pgnbgreunbgrlem5lem3  49435  grlimedgnedg  49444  2arymaptf1  49980