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 2793	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  preq12i  4743  preq12d  4746  ssprsseq  4829  preq12b  4852  prnebg  4857  preq12nebg  4864  opthprneg  4866  relop  5851  opthreg  9613  hashle2pr  14438  wwlktovfo  14909  joinval  18330  meetval  18344  ipole  18487  sylow1  19471  frgpuplem  19640  uspgr2wlkeq  28934  wlkres  28958  wlkp1lem8  28968  usgr2pthlem  29051  2wlkdlem10  29220  1wlkdlem4  29424  3wlkdlem6  29449  3wlkdlem10  29453  pfxwlk  34145  oppr  45788  imarnf1pr  46038  elsprel  46191  sprsymrelf1lem  46207  sprsymrelf  46211  paireqne  46227  sbcpr  46237  isomuspgrlem2b  46545  isomuspgrlem2d  46547