Theorem preq12 4631

Description: Equality theorem for unordered pairs. (Contributed by NM, 19-Oct-2012.)

Assertion

Ref	Expression
preq12	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Proof of Theorem preq12

Step	Hyp	Ref	Expression
1		preq1 4629	. 2 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2		preq2 4630	. 2 ⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
3	1, 2	sylan9eq 2853	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538  {cpr 4527

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-sn 4526  df-pr 4528

This theorem is referenced by:  preq12i  4634  preq12d  4637  ssprsseq  4718  preq12b  4741  prnebg  4746  preq12nebg  4753  opthprneg  4755  snex  5297  relop  5685  opthreg  9065  hashle2pr  13831  wwlktovfo  14313  joinval  17607  meetval  17621  ipole  17760  sylow1  18720  frgpuplem  18890  uspgr2wlkeq  27435  wlkres  27460  wlkp1lem8  27470  usgr2pthlem  27552  2wlkdlem10  27721  1wlkdlem4  27925  3wlkdlem6  27950  3wlkdlem10  27954  pfxwlk  32483  oppr  43622  imarnf1pr  43838  elsprel  43992  sprsymrelf1lem  44008  sprsymrelf  44012  paireqne  44028  sbcpr  44038  isomuspgrlem2b  44347  isomuspgrlem2d  44349