Theorem preq1d 4418

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

Syntax hints:   → wi 4   = wceq 1632  {cpr 4323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-un 3720  df-sn 4322  df-pr 4324

This theorem is referenced by:  propeqop  5118  opthwiener  5124  fprg  6585  fnpr2g  6638  dfac2b  9143  dfac2OLD  9145  symg2bas  18018  crctcshwlkn0lem6  26918  wwlksnredwwlkn  27013  wwlksnextprop  27030  clwwlk1loop  27111  clwlkclwwlklem2fv1  27118  clwlkclwwlklem2fv2  27119  clwlkclwwlklem2a  27121  clwlkclwwlklem3  27124  clwwisshclwwslem  27137  clwwlknlbonbgr1  27168  clwwlkn1  27170  frcond1  27420  frgr1v  27425  nfrgr2v  27426  frgr3v  27429  n4cyclfrgr  27445  2clwwlk2clwwlklem  27503  fprb  31976  wopprc  38099