Theorem preq2d 4632

Description: Equality deduction for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Hypothesis

Ref	Expression
preq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
preq2d	⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Proof of Theorem preq2d

Step	Hyp	Ref	Expression
1		preq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		preq2 4626	. 2 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1542  {cpr 4519

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 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-un 3849  df-sn 4518  df-pr 4520

This theorem is referenced by:  opeq2  4762  opeq2OLD  4763  opthwiener  5372  fprg  6928  fprb  6967  fnprb  6982  fnpr2g  6984  opthreg  9155  fzosplitprm1  13239  s2prop  14359  gsumprval  18015  indislem  21752  isconn  22165  hmphindis  22549  wilthlem2  25806  ispth  27664  wwlksnredwwlkn  27833  wwlksnextfun  27836  wwlksnextinj  27837  wwlksnextsurj  27838  wwlksnextbij  27840  clwlkclwwlklem2a1  27929  clwlkclwwlklem2a4  27934  clwlkclwwlklem2  27937  clwwisshclwwslemlem  27950  clwwlkn2  27981  clwwlkf  27984  clwwlknonex2lem1  28044  eupth2lem3lem3  28167  eupth2  28176  frcond1  28203  nfrgr2v  28209  frgr3v  28212  n4cyclfrgr  28228  measxun2  31748  altopthsn  33901  mapdindp4  39357  isomuspgrlem2d  44809  2arymaptf1  45525  rrx2xpref1o  45590