Theorem preq12 4691

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-sn 4580  df-pr 4582

This theorem is referenced by:  preq12i  4694  preq12d  4697  ssprsseq  4780  preq12b  4805  prnebg  4811  preq12nebg  4818  opthprneg  4820  elpr2elpr  4824  relop  5818  opthreg  9567  hashle2pr  14484  wwlktovfo  14965  joinval  18398  meetval  18412  ipole  18557  sylow1  19634  frgpuplem  19803  uspgr2wlkeq  29803  wlkres  29826  wlkp1lem8  29836  usgr2pthlem  29920  2wlkdlem10  30092  1wlkdlem4  30299  3wlkdlem6  30324  3wlkdlem10  30328  pfxwlk  35435  oppr  47585  imarnf1pr  47837  elsprel  48042  sprsymrelf1lem  48058  sprsymrelf  48062  paireqne  48078  sbcpr  48088  isuspgrimlem  48478  grtrif1o  48525