Theorem preq1d 4696

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  propeqop  5478  opthwiener  5486  fprg  7160  fprb  7200  fnpr2g  7217  dif1en  9181  dfac2b  10213  symg2bas  19613  crctcshwlkn0lem6  30410  wwlksnredwwlkn  30490  wwlksnextprop  30507  clwwlk1loop  30585  clwlkclwwlklem2fv1  30592  clwlkclwwlklem2fv2  30593  clwlkclwwlklem2a  30595  clwlkclwwlklem3  30598  clwwisshclwwslem  30611  clwwlknlbonbgr1  30636  clwwlkn1  30638  frcond1  30873  frgr1v  30878  nfrgr2v  30879  frgr3v  30882  n4cyclfrgr  30898  2clwwlk2clwwlklem  30953  wopprc  44131  mnurndlem1  45359  grtriclwlk3  49137  isubgr3stgrlem4  49161  gpgedgiov  49257  gpgedg2ov  49258  gpgedg2iv  49259  pgnbgreunbgrlem5lem1  49312  pgnbgreunbgrlem5lem2  49313  pgnbgreunbgrlem5lem3  49314  grlimedgnedg  49323  2arymaptf1  49859