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 2815	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 2732

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 2739  df-cleq 2752  df-clel 2835  df-v 3452  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  5830  opthreg  9597  hashle2pr  14542  wwlktovfo  15031  joinval  18463  meetval  18477  ipole  18622  sylow1  19730  frgpuplem  19899  uspgr2wlkeq  30105  wlkres  30128  wlkp1lem8  30138  pfxwlk  30145  usgr2pthlem  30228  2wlkdlem10  30403  1wlkdlem4  30610  3wlkdlem6  30645  3wlkdlem10  30649  oppr  47918  imarnf1pr  48170  elsprel  48375  sprsymrelf1lem  48391  sprsymrelf  48395  paireqne  48411  sbcpr  48421  isuspgrimlem  48811  grtrif1o  48858