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

Theorem preq12 4701
Description: Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)
Assertion
Ref Expression
preq12 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Proof of Theorem preq12
StepHypRef Expression
1 preq1 4699 . 2 (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2 preq2 4700 . 2 (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
31, 2sylan9eq 2797 1 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397   = wceq 1542  {cpr 4593
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 2708
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 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-un 3920  df-sn 4592  df-pr 4594
This theorem is referenced by:  preq12i  4704  preq12d  4707  ssprsseq  4790  preq12b  4813  prnebg  4818  preq12nebg  4825  opthprneg  4827  relop  5811  opthreg  9561  hashle2pr  14383  wwlktovfo  14854  joinval  18273  meetval  18287  ipole  18430  sylow1  19392  frgpuplem  19561  uspgr2wlkeq  28636  wlkres  28660  wlkp1lem8  28670  usgr2pthlem  28753  2wlkdlem10  28922  1wlkdlem4  29126  3wlkdlem6  29151  3wlkdlem10  29155  pfxwlk  33757  oppr  45338  imarnf1pr  45588  elsprel  45741  sprsymrelf1lem  45757  sprsymrelf  45761  paireqne  45777  sbcpr  45787  isomuspgrlem2b  46095  isomuspgrlem2d  46097
  Copyright terms: Public domain W3C validator