Theorem preq1d 4678

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

Syntax hints:   → wi 4   = wceq 1547  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  propeqop  5455  opthwiener  5462  fprg  7105  fprb  7145  fnpr2g  7161  dif1en  9093  dfac2b  10051  symg2bas  19366  crctcshwlkn0lem6  29908  wwlksnredwwlkn  29988  wwlksnextprop  30005  clwwlk1loop  30083  clwlkclwwlklem2fv1  30090  clwlkclwwlklem2fv2  30091  clwlkclwwlklem2a  30093  clwlkclwwlklem3  30096  clwwisshclwwslem  30109  clwwlknlbonbgr1  30134  clwwlkn1  30136  frcond1  30361  frgr1v  30366  nfrgr2v  30367  frgr3v  30370  n4cyclfrgr  30386  2clwwlk2clwwlklem  30441  wopprc  43482  mnurndlem1  44732  grtriclwlk3  48443  isubgr3stgrlem4  48467  gpgedgiov  48563  gpgedg2ov  48564  gpgedg2iv  48565  pgnbgreunbgrlem5lem1  48618  pgnbgreunbgrlem5lem2  48619  pgnbgreunbgrlem5lem3  48620  grlimedgnedg  48629  2arymaptf1  49151  rrx2xpref1o  49216