Theorem preq1d 4675

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

Syntax hints:   → wi 4   = wceq 1537  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-sn 4568  df-pr 4570

This theorem is referenced by:  propeqop  5397  opthwiener  5404  fprg  6917  fprb  6956  fnpr2g  6973  dfac2b  9556  symg2bas  18521  crctcshwlkn0lem6  27593  wwlksnredwwlkn  27673  wwlksnextprop  27691  clwwlk1loop  27766  clwlkclwwlklem2fv1  27773  clwlkclwwlklem2fv2  27774  clwlkclwwlklem2a  27776  clwlkclwwlklem3  27779  clwwisshclwwslem  27792  clwwlknlbonbgr1  27817  clwwlkn1  27819  frcond1  28045  frgr1v  28050  nfrgr2v  28051  frgr3v  28054  n4cyclfrgr  28070  2clwwlk2clwwlklem  28125  wopprc  39647  mnurndlem1  40637  isomuspgrlem2d  44016  rrx2xpref1o  44725