Theorem preq12 4668

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 4666	. 2 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2		preq2 4667	. 2 ⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
3	1, 2	sylan9eq 2799	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  preq12i  4671  preq12d  4674  ssprsseq  4755  preq12b  4778  prnebg  4783  preq12nebg  4790  opthprneg  4792  snex  5349  relop  5748  opthreg  9306  hashle2pr  14119  wwlktovfo  14601  joinval  18010  meetval  18024  ipole  18167  sylow1  19123  frgpuplem  19293  uspgr2wlkeq  27915  wlkres  27940  wlkp1lem8  27950  usgr2pthlem  28032  2wlkdlem10  28201  1wlkdlem4  28405  3wlkdlem6  28430  3wlkdlem10  28434  pfxwlk  32985  oppr  44411  imarnf1pr  44661  elsprel  44815  sprsymrelf1lem  44831  sprsymrelf  44835  paireqne  44851  sbcpr  44861  isomuspgrlem2b  45169  isomuspgrlem2d  45171