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

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

Proof of Theorem preq12
StepHypRef Expression
1 preq1 4692 . 2 (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2 preq2 4693 . 2 (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
31, 2sylan9eq 2797 1 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  {cpr 4586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-un 3913  df-sn 4585  df-pr 4587
This theorem is referenced by:  preq12i  4697  preq12d  4700  ssprsseq  4783  preq12b  4806  prnebg  4811  preq12nebg  4818  opthprneg  4820  relop  5804  opthreg  9512  hashle2pr  14330  wwlktovfo  14807  joinval  18226  meetval  18240  ipole  18383  sylow1  19344  frgpuplem  19513  uspgr2wlkeq  28423  wlkres  28447  wlkp1lem8  28457  usgr2pthlem  28540  2wlkdlem10  28709  1wlkdlem4  28913  3wlkdlem6  28938  3wlkdlem10  28942  pfxwlk  33529  oppr  45165  imarnf1pr  45415  elsprel  45568  sprsymrelf1lem  45584  sprsymrelf  45588  paireqne  45604  sbcpr  45614  isomuspgrlem2b  45922  isomuspgrlem2d  45924
  Copyright terms: Public domain W3C validator