Theorem preq12 4270

Description: Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Assertion

Ref	Expression
preq12	|- ( ( A = C /\ B = D ) -> { A , B } = { C , D } )

Proof of Theorem preq12

Step	Hyp	Ref	Expression
1		preq1 4268	. 2 |- ( A = C -> { A , B } = { C , B } )
2		preq2 4269	. 2 |- ( B = D -> { C , B } = { C , D } )
3	1, 2	sylan9eq 2676	1 |- ( ( A = C /\ B = D ) -> { A , B } = { C , D } )

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   {cpr 4179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-sn 4178  df-pr 4180

This theorem is referenced by:  preq12i  4273  preq12d  4276  ssprsseq  4357  preq12b  4382  prnebg  4389  snex  4908  relop  5272  opthreg  8515  hashle2pr  13259  wwlktovfo  13701  joinval  17005  meetval  17019  ipole  17158  sylow1  18018  frgpuplem  18185  uspgr2wlkeq  26542  wlkres  26567  wlkp1lem8  26577  usgr2pthlem  26659  2wlkdlem10  26831  1wlkdlem4  27000  3wlkdlem6  27025  3wlkdlem10  27029  imarnf1pr  41301  elsprel  41725  sprsymrelf1lem  41741  sprsymrelf  41745