Theorem preq1d 4701

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

Syntax hints:   → wi 4   = wceq 1563  {cpr 4587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3912  df-sn 4586  df-pr 4588

This theorem is referenced by:  propeqop  5481  opthwiener  5488  fprg  7142  fprb  7182  fnpr2g  7198  dif1en  9134  dfac2b  10102  symg2bas  19454  crctcshwlkn0lem6  30073  wwlksnredwwlkn  30153  wwlksnextprop  30170  clwwlk1loop  30248  clwlkclwwlklem2fv1  30255  clwlkclwwlklem2fv2  30256  clwlkclwwlklem2a  30258  clwlkclwwlklem3  30261  clwwisshclwwslem  30274  clwwlknlbonbgr1  30299  clwwlkn1  30301  frcond1  30526  frgr1v  30531  nfrgr2v  30532  frgr3v  30535  n4cyclfrgr  30551  2clwwlk2clwwlklem  30606  wopprc  43619  mnurndlem1  44855  grtriclwlk3  48565  isubgr3stgrlem4  48589  gpgedgiov  48685  gpgedg2ov  48686  gpgedg2iv  48687  pgnbgreunbgrlem5lem1  48740  pgnbgreunbgrlem5lem2  48741  pgnbgreunbgrlem5lem3  48742  grlimedgnedg  48751  2arymaptf1  49284  rrx2xpref1o  49349