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

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

Proof of Theorem preq12
StepHypRef Expression
1 preq1 4733 . 2 (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2 preq2 4734 . 2 (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
31, 2sylan9eq 2797 1 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1540  {cpr 4628
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629
This theorem is referenced by:  preq12i  4738  preq12d  4741  ssprsseq  4825  preq12b  4850  prnebg  4856  preq12nebg  4863  opthprneg  4865  elpr2elpr  4869  relop  5861  opthreg  9658  hashle2pr  14516  wwlktovfo  14997  joinval  18422  meetval  18436  ipole  18579  sylow1  19621  frgpuplem  19790  uspgr2wlkeq  29664  wlkres  29688  wlkp1lem8  29698  usgr2pthlem  29783  2wlkdlem10  29955  1wlkdlem4  30159  3wlkdlem6  30184  3wlkdlem10  30188  pfxwlk  35129  oppr  47042  imarnf1pr  47294  elsprel  47462  sprsymrelf1lem  47478  sprsymrelf  47482  paireqne  47498  sbcpr  47508  isuspgrimlem  47874  grtrif1o  47909
  Copyright terms: Public domain W3C validator