Theorem preq12 4689

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  preq12i  4692  preq12d  4695  ssprsseq  4779  preq12b  4804  prnebg  4810  preq12nebg  4817  opthprneg  4819  elpr2elpr  4823  relop  5797  opthreg  9533  hashle2pr  14402  wwlktovfo  14883  joinval  18299  meetval  18313  ipole  18458  sylow1  19500  frgpuplem  19669  uspgr2wlkeq  29609  wlkres  29632  wlkp1lem8  29642  usgr2pthlem  29726  2wlkdlem10  29898  1wlkdlem4  30102  3wlkdlem6  30127  3wlkdlem10  30131  pfxwlk  35099  oppr  47018  imarnf1pr  47270  elsprel  47463  sprsymrelf1lem  47479  sprsymrelf  47483  paireqne  47499  sbcpr  47509  isuspgrimlem  47883  grtrif1o  47930