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  28903  wlkres  28927  wlkp1lem8  28937  usgr2pthlem  29020  2wlkdlem10  29189  1wlkdlem4  29393  3wlkdlem6  29418  3wlkdlem10  29422  pfxwlk  34114  oppr  45740  imarnf1pr  45990  elsprel  46143  sprsymrelf1lem  46159  sprsymrelf  46163  paireqne  46179  sbcpr  46189  isomuspgrlem2b  46497  isomuspgrlem2d  46499