Theorem preq12 4671

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

Assertion

Ref	Expression
preq12	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Proof of Theorem preq12

Step	Hyp	Ref	Expression
1		preq1 4669	. 2 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2		preq2 4670	. 2 ⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
3	1, 2	sylan9eq 2798	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-sn 4562  df-pr 4564

This theorem is referenced by:  preq12i  4674  preq12d  4677  ssprsseq  4758  preq12b  4781  prnebg  4786  preq12nebg  4793  opthprneg  4795  snex  5354  relop  5759  opthreg  9376  hashle2pr  14191  wwlktovfo  14673  joinval  18095  meetval  18109  ipole  18252  sylow1  19208  frgpuplem  19378  uspgr2wlkeq  28013  wlkres  28038  wlkp1lem8  28048  usgr2pthlem  28131  2wlkdlem10  28300  1wlkdlem4  28504  3wlkdlem6  28529  3wlkdlem10  28533  pfxwlk  33085  oppr  44524  imarnf1pr  44774  elsprel  44927  sprsymrelf1lem  44943  sprsymrelf  44947  paireqne  44963  sbcpr  44973  isomuspgrlem2b  45281  isomuspgrlem2d  45283