Theorem preq12 4702

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  preq12i  4705  preq12d  4708  ssprsseq  4792  preq12b  4816  prnebg  4822  preq12nebg  4829  opthprneg  4831  elpr2elpr  4835  relop  5838  opthreg  9588  hashle2pr  14516  wwlktovfo  14997  joinval  18432  meetval  18446  ipole  18591  sylow1  19674  frgpuplem  19843  uspgr2wlkeq  29976  wlkres  29999  wlkp1lem8  30009  usgr2pthlem  30093  2wlkdlem10  30265  1wlkdlem4  30472  3wlkdlem6  30497  3wlkdlem10  30501  pfxwlk  35597  oppr  47750  imarnf1pr  48002  elsprel  48207  sprsymrelf1lem  48223  sprsymrelf  48227  paireqne  48243  sbcpr  48253  isuspgrimlem  48643  grtrif1o  48690