Theorem preq1d 4703

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-un 3907  df-sn 4588  df-pr 4590

This theorem is used by:  propeqop  5488  opthwiener  5495  fprg  7156  fprb  7196  fnpr2g  7213  dif1en  9160  dfac2b  10137  symg2bas  19526  crctcshwlkn0lem6  30291  wwlksnredwwlkn  30371  wwlksnextprop  30388  clwwlk1loop  30466  clwlkclwwlklem2fv1  30473  clwlkclwwlklem2fv2  30474  clwlkclwwlklem2a  30476  clwlkclwwlklem3  30479  clwwisshclwwslem  30492  clwwlknlbonbgr1  30517  clwwlkn1  30519  frcond1  30754  frgr1v  30759  nfrgr2v  30760  frgr3v  30763  n4cyclfrgr  30779  2clwwlk2clwwlklem  30834  wopprc  43879  mnurndlem1  45113  grtriclwlk3  48869  isubgr3stgrlem4  48893  gpgedgiov  48989  gpgedg2ov  48990  gpgedg2iv  48991  pgnbgreunbgrlem5lem1  49044  pgnbgreunbgrlem5lem2  49045  pgnbgreunbgrlem5lem3  49046  grlimedgnedg  49055  2arymaptf1  49591  rrx2xpref1o  49656