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 2785	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  preq12i  4705  preq12d  4708  ssprsseq  4792  preq12b  4817  prnebg  4823  preq12nebg  4830  opthprneg  4832  elpr2elpr  4836  relop  5817  opthreg  9578  hashle2pr  14449  wwlktovfo  14931  joinval  18343  meetval  18357  ipole  18500  sylow1  19540  frgpuplem  19709  uspgr2wlkeq  29581  wlkres  29605  wlkp1lem8  29615  usgr2pthlem  29700  2wlkdlem10  29872  1wlkdlem4  30076  3wlkdlem6  30101  3wlkdlem10  30105  pfxwlk  35118  oppr  47035  imarnf1pr  47287  elsprel  47480  sprsymrelf1lem  47496  sprsymrelf  47500  paireqne  47516  sbcpr  47526  isuspgrimlem  47899  grtrif1o  47945