Theorem preq12 4692

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4150  df-sn 4585  df-pr 4587

This theorem is used by:  preq12i  4695  preq12d  4698  ssprsseq  4780  preq12b  4804  prnebg  4810  preq12nebg  4817  opthprneg  4819  elpr2elpr  4823  relop  5828  opthreg  9624  hashle2pr  14627  wwlktovfo  15118  joinval  18556  meetval  18570  ipole  18715  sylow1  19824  frgpuplem  19993  uspgr2wlkeq  30233  wlkres  30256  wlkp1lem8  30266  pfxwlk  30273  usgr2pthlem  30356  2wlkdlem10  30531  1wlkdlem4  30738  3wlkdlem6  30773  3wlkdlem10  30777  oppr  48207  imarnf1pr  48459  elsprel  48664  sprsymrelf1lem  48680  sprsymrelf  48684  paireqne  48700  sbcpr  48710  isuspgrimlem  49100  grtrif1o  49147