Theorem preq12 4696

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  preq12i  4699  preq12d  4702  ssprsseq  4786  preq12b  4810  prnebg  4816  preq12nebg  4823  opthprneg  4825  elpr2elpr  4829  relop  5828  opthreg  9612  hashle2pr  14615  wwlktovfo  15104  joinval  18542  meetval  18556  ipole  18701  sylow1  19810  frgpuplem  19979  uspgr2wlkeq  30219  wlkres  30242  wlkp1lem8  30252  pfxwlk  30259  usgr2pthlem  30342  2wlkdlem10  30517  1wlkdlem4  30724  3wlkdlem6  30759  3wlkdlem10  30763  oppr  48069  imarnf1pr  48321  elsprel  48526  sprsymrelf1lem  48542  sprsymrelf  48546  paireqne  48562  sbcpr  48572  isuspgrimlem  48962  grtrif1o  49009