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

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

Proof of Theorem preq12
StepHypRef Expression
1 preq1 4404 . 2 (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2 preq2 4405 . 2 (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
31, 2sylan9eq 2806 1 ((𝐴 = 𝐶𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1624  {cpr 4315 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-v 3334  df-un 3712  df-sn 4314  df-pr 4316 This theorem is referenced by:  preq12i  4409  preq12d  4412  ssprsseq  4494  preq12b  4518  prnebg  4525  preq12nebg  4535  opthprneg  4537  snex  5049  relop  5420  opthreg  8678  opthregOLD  8680  hashle2pr  13443  wwlktovfo  13894  joinval  17198  meetval  17212  ipole  17351  sylow1  18210  frgpuplem  18377  uspgr2wlkeq  26744  wlkres  26769  wlkp1lem8  26779  usgr2pthlem  26861  2wlkdlem10  27047  1wlkdlem4  27284  3wlkdlem6  27309  3wlkdlem10  27313  imarnf1pr  41801  elsprel  42227  sprsymrelf1lem  42243  sprsymrelf  42247
 Copyright terms: Public domain W3C validator