Theorem preq12 4740

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-sn 4632  df-pr 4634

This theorem is referenced by:  preq12i  4743  preq12d  4746  ssprsseq  4830  preq12b  4855  prnebg  4861  preq12nebg  4868  opthprneg  4870  elpr2elpr  4874  relop  5864  opthreg  9656  hashle2pr  14513  wwlktovfo  14994  joinval  18435  meetval  18449  ipole  18592  sylow1  19636  frgpuplem  19805  uspgr2wlkeq  29679  wlkres  29703  wlkp1lem8  29713  usgr2pthlem  29796  2wlkdlem10  29965  1wlkdlem4  30169  3wlkdlem6  30194  3wlkdlem10  30198  pfxwlk  35108  oppr  46980  imarnf1pr  47232  elsprel  47400  sprsymrelf1lem  47416  sprsymrelf  47420  paireqne  47436  sbcpr  47446  isuspgrimlem  47812  grtrif1o  47847