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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-pr 4580

This theorem is referenced by:  preq12i  4692  preq12d  4695  ssprsseq  4778  preq12b  4803  prnebg  4809  preq12nebg  4816  opthprneg  4818  elpr2elpr  4822  relop  5796  opthreg  9517  hashle2pr  14388  wwlktovfo  14869  joinval  18285  meetval  18299  ipole  18444  sylow1  19519  frgpuplem  19688  uspgr2wlkeq  29628  wlkres  29651  wlkp1lem8  29661  usgr2pthlem  29745  2wlkdlem10  29917  1wlkdlem4  30124  3wlkdlem6  30149  3wlkdlem10  30153  pfxwlk  35191  oppr  47157  imarnf1pr  47409  elsprel  47602  sprsymrelf1lem  47618  sprsymrelf  47622  paireqne  47638  sbcpr  47648  isuspgrimlem  48022  grtrif1o  48069