MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  preq12 Structured version   Unicode version

Theorem preq12 4097
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
StepHypRef Expression
1 preq1 4095 . 2  |-  ( A  =  C  ->  { A ,  B }  =  { C ,  B }
)
2 preq2 4096 . 2  |-  ( B  =  D  ->  { C ,  B }  =  { C ,  D }
)
31, 2sylan9eq 2515 1  |-  ( ( A  =  C  /\  B  =  D )  ->  { A ,  B }  =  { C ,  D } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1398   {cpr 4018
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-sn 4017  df-pr 4019
This theorem is referenced by:  preq12i  4100  preq12d  4103  preq12b  4192  prnebg  4198  snex  4678  relop  5142  opthreg  8026  hash2prd  12505  wwlktovfo  12890  joinval  15837  meetval  15851  ipole  15990  sylow1  16825  frgpuplem  16992  sizeusglecusglem1  24689  3v3e3cycl1  24849  4cycl4v4e  24871  4cycl4dv4e  24873  usg2wlkeq  24913  usg2wlkonot  25088  imarnf1pr  32702  usgra2pthlem1  32744
  Copyright terms: Public domain W3C validator