Theorem preq12 4711

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540  {cpr 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-pr 4604

This theorem is referenced by:  preq12i  4714  preq12d  4717  ssprsseq  4801  preq12b  4826  prnebg  4832  preq12nebg  4839  opthprneg  4841  elpr2elpr  4845  relop  5830  opthreg  9632  hashle2pr  14495  wwlktovfo  14977  joinval  18387  meetval  18401  ipole  18544  sylow1  19584  frgpuplem  19753  uspgr2wlkeq  29626  wlkres  29650  wlkp1lem8  29660  usgr2pthlem  29745  2wlkdlem10  29917  1wlkdlem4  30121  3wlkdlem6  30146  3wlkdlem10  30150  pfxwlk  35146  oppr  47059  imarnf1pr  47311  elsprel  47489  sprsymrelf1lem  47505  sprsymrelf  47509  paireqne  47525  sbcpr  47535  isuspgrimlem  47908  grtrif1o  47954