Theorem preq12 4735

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629

This theorem is referenced by:  preq12i  4738  preq12d  4741  ssprsseq  4825  preq12b  4850  prnebg  4856  preq12nebg  4863  opthprneg  4865  elpr2elpr  4869  relop  5861  opthreg  9658  hashle2pr  14516  wwlktovfo  14997  joinval  18422  meetval  18436  ipole  18579  sylow1  19621  frgpuplem  19790  uspgr2wlkeq  29664  wlkres  29688  wlkp1lem8  29698  usgr2pthlem  29783  2wlkdlem10  29955  1wlkdlem4  30159  3wlkdlem6  30184  3wlkdlem10  30188  pfxwlk  35129  oppr  47042  imarnf1pr  47294  elsprel  47462  sprsymrelf1lem  47478  sprsymrelf  47482  paireqne  47498  sbcpr  47508  isuspgrimlem  47874  grtrif1o  47909