Theorem preq12 4692

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  preq12i  4695  preq12d  4698  ssprsseq  4781  preq12b  4806  prnebg  4812  preq12nebg  4819  opthprneg  4821  elpr2elpr  4825  relop  5799  opthreg  9527  hashle2pr  14400  wwlktovfo  14881  joinval  18298  meetval  18312  ipole  18457  sylow1  19532  frgpuplem  19701  uspgr2wlkeq  29719  wlkres  29742  wlkp1lem8  29752  usgr2pthlem  29836  2wlkdlem10  30008  1wlkdlem4  30215  3wlkdlem6  30240  3wlkdlem10  30244  pfxwlk  35318  oppr  47276  imarnf1pr  47528  elsprel  47721  sprsymrelf1lem  47737  sprsymrelf  47741  paireqne  47757  sbcpr  47767  isuspgrimlem  48141  grtrif1o  48188