Theorem preq12 4406

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 4404	. 2 ⊢ (𝐴 = 𝐶 → {𝐴, 𝐵} = {𝐶, 𝐵})
2		preq2 4405	. 2 ⊢ (𝐵 = 𝐷 → {𝐶, 𝐵} = {𝐶, 𝐷})
3	1, 2	sylan9eq 2806	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐷) → {𝐴, 𝐵} = {𝐶, 𝐷})

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