Theorem preq12 4698

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  preq12i  4701  preq12d  4704  ssprsseq  4786  preq12b  4810  prnebg  4816  preq12nebg  4823  opthprneg  4825  elpr2elpr  4829  relop  5838  opthreg  9656  hashle2pr  14663  wwlktovfo  15154  joinval  18599  meetval  18613  ipole  18758  sylow1  19868  frgpuplem  20037  uspgr2wlkeq  30283  wlkres  30306  wlkp1lem8  30316  pfxwlk  30323  usgr2pthlem  30406  2wlkdlem10  30581  1wlkdlem4  30788  3wlkdlem6  30823  3wlkdlem10  30827  oppr  48373  imarnf1pr  48625  elsprel  48830  sprsymrelf1lem  48846  sprsymrelf  48850  paireqne  48866  sbcpr  48876  isuspgrimlem  49266  grtrif1o  49313