Theorem preq12 4760

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537  {cpr 4650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-sn 4649  df-pr 4651

This theorem is referenced by:  preq12i  4763  preq12d  4766  ssprsseq  4850  preq12b  4875  prnebg  4880  preq12nebg  4887  opthprneg  4889  elpr2elpr  4893  relop  5875  opthreg  9687  hashle2pr  14526  wwlktovfo  15007  joinval  18447  meetval  18461  ipole  18604  sylow1  19645  frgpuplem  19814  uspgr2wlkeq  29682  wlkres  29706  wlkp1lem8  29716  usgr2pthlem  29799  2wlkdlem10  29968  1wlkdlem4  30172  3wlkdlem6  30197  3wlkdlem10  30201  pfxwlk  35091  oppr  46945  imarnf1pr  47197  elsprel  47349  sprsymrelf1lem  47365  sprsymrelf  47369  paireqne  47385  sbcpr  47395  isuspgrimlem  47758  grtrif1o  47793