Theorem preq1d 4704

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

Syntax hints:   → wi 4   = wceq 1568  {cpr 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-sn 4589  df-pr 4591

This theorem is referenced by:  propeqop  5490  opthwiener  5497  fprg  7152  fprb  7192  fnpr2g  7208  dif1en  9145  dfac2b  10113  symg2bas  19462  crctcshwlkn0lem6  30130  wwlksnredwwlkn  30210  wwlksnextprop  30227  clwwlk1loop  30305  clwlkclwwlklem2fv1  30312  clwlkclwwlklem2fv2  30313  clwlkclwwlklem2a  30315  clwlkclwwlklem3  30318  clwwisshclwwslem  30331  clwwlknlbonbgr1  30356  clwwlkn1  30358  frcond1  30583  frgr1v  30588  nfrgr2v  30589  frgr3v  30592  n4cyclfrgr  30608  2clwwlk2clwwlklem  30663  wopprc  43705  mnurndlem1  44939  grtriclwlk3  48655  isubgr3stgrlem4  48679  gpgedgiov  48775  gpgedg2ov  48776  gpgedg2iv  48777  pgnbgreunbgrlem5lem1  48830  pgnbgreunbgrlem5lem2  48831  pgnbgreunbgrlem5lem3  48832  grlimedgnedg  48841  2arymaptf1  49378  rrx2xpref1o  49443