Theorem preq12 4111

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 4109	. 2
2		preq2 4110	. 2
3	1, 2	sylan9eq 2518	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  {cpr 4031

This theorem is referenced by:  preq12i  4114  preq12d  4117  preq12b  4206  prnebg  4212  snex  4693  relop  5158  opthreg  8056  hash2prd  12518  wwlktovfo  12896  joinval  15635  meetval  15649  ipole  15788  sylow1  16623  frgpuplem  16790  sizeusglecusglem1  24484  3v3e3cycl1  24644  4cycl4v4e  24666  4cycl4dv4e  24668  usg2wlkeq  24708  usg2wlkonot  24883  imarnf1pr  32309  usgra2pthlem1  32353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032