Theorem preq1d 4274

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

Syntax hints:   → wi 4   = wceq 1483  {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  propeqop  4970  opthwiener  4976  fprg  6422  fnpr2g  6474  dfac2  8953  symg2bas  17818  crctcshwlkn0lem6  26707  wwlksnredwwlkn  26790  wwlksnextprop  26807  clwlkclwwlklem2fv1  26896  clwlkclwwlklem2fv2  26897  clwlkclwwlklem2a  26899  clwlkclwwlklem3  26902  clwwlks1loop  26908  clwwlksn1loop  26909  clwwisshclwwslem  26927  frcond1  27130  frgr1v  27135  nfrgr2v  27136  frgr3v  27139  n4cyclfrgr  27155  fprb  31669  wopprc  37597