Theorem preq12 4674

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  preq12i  4677  preq12d  4680  ssprsseq  4763  preq12b  4788  prnebg  4794  preq12nebg  4801  opthprneg  4803  elpr2elpr  4807  relop  5799  opthreg  9537  hashle2pr  14437  wwlktovfo  14918  joinval  18339  meetval  18353  ipole  18498  sylow1  19576  frgpuplem  19745  uspgr2wlkeq  29739  wlkres  29762  wlkp1lem8  29772  usgr2pthlem  29856  2wlkdlem10  30028  1wlkdlem4  30235  3wlkdlem6  30260  3wlkdlem10  30264  pfxwlk  35359  oppr  47500  imarnf1pr  47752  elsprel  47957  sprsymrelf1lem  47973  sprsymrelf  47977  paireqne  47993  sbcpr  48003  isuspgrimlem  48393  grtrif1o  48440