Theorem preq12 4699

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

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

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 3449  df-un 3919  df-sn 4590  df-pr 4592

This theorem is referenced by:  preq12i  4702  preq12d  4705  ssprsseq  4789  preq12b  4814  prnebg  4820  preq12nebg  4827  opthprneg  4829  elpr2elpr  4833  relop  5814  opthreg  9571  hashle2pr  14442  wwlktovfo  14924  joinval  18336  meetval  18350  ipole  18493  sylow1  19533  frgpuplem  19702  uspgr2wlkeq  29574  wlkres  29598  wlkp1lem8  29608  usgr2pthlem  29693  2wlkdlem10  29865  1wlkdlem4  30069  3wlkdlem6  30094  3wlkdlem10  30098  pfxwlk  35111  oppr  47031  imarnf1pr  47283  elsprel  47476  sprsymrelf1lem  47492  sprsymrelf  47496  paireqne  47512  sbcpr  47522  isuspgrimlem  47895  grtrif1o  47941