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

Theorem preq12 4040
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 4038 . 2  |-  ( A  =  C  ->  { A ,  B }  =  { C ,  B }
)
2 preq2 4039 . 2  |-  ( B  =  D  ->  { C ,  B }  =  { C ,  D }
)
31, 2sylan9eq 2510 1  |-  ( ( A  =  C  /\  B  =  D )  ->  { A ,  B }  =  { C ,  D } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1370   {cpr 3963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2429
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1702  df-clab 2436  df-cleq 2442  df-clel 2445  df-nfc 2598  df-v 3056  df-un 3417  df-sn 3962  df-pr 3964
This theorem is referenced by:  preq12i  4043  preq12d  4046  preq12b  4132  prnebg  4138  snex  4617  relop  5074  opthreg  7911  hash2prd  12269  joinval  15263  meetval  15277  ipole  15416  sylow1  16192  frgpuplem  16359  sizeusglecusglem1  23513  3v3e3cycl1  23651  4cycl4v4e  23673  4cycl4dv4e  23675  imarnf1pr  30274  wwlktovfo  30377  usg2wlkeq  30413  usgra2pthlem1  30424  usg2wlkonot  30526
  Copyright terms: Public domain W3C validator