Theorem preq2 3960

Description: Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
preq2	|- ( A = B -> { C , A } = { C , B } )

Proof of Theorem preq2

Step	Hyp	Ref	Expression
1		preq1 3959	. 2 |- ( A = B -> { A , C } = { B , C } )
2		prcom 3958	. 2 |- { C , A } = { A , C }
3		prcom 3958	. 2 |- { C , B } = { B , C }
4	1, 2, 3	3eqtr4g 2500	1 |- ( A = B -> { C , A } = { C , B } )

Syntax hints:   -> wi 4   = wceq 1369   {cpr 3884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-un 3338  df-sn 3883  df-pr 3885

This theorem is referenced by:  preq12  3961  preq2i  3963  preq2d  3966  tpeq2  3969  preq12bg  4056  prel12g  4057  opeq2  4065  uniprg  4110  intprg  4167  prex  4539  opth  4571  opeqsn  4592  relop  4995  funopg  5455  f1oprswap  5685  fprg  5896  fnprb  5941  pr2ne  8177  prdom2  8178  dfac2  8305  brdom7disj  8703  brdom6disj  8704  wunpr  8881  wunex2  8910  wuncval2  8919  grupr  8969  prunioo  11419  hashprg  12160  isprm2lem  13775  joindef  15179  meetdef  15193  lspfixed  17214  hmphindis  19375  umgraex  23262  usgraedg4  23310  usgraedgreu  23311  nbgrael  23342  nbgraeledg  23346  nbgranself  23350  nbgraf1olem4  23358  nb3graprlem1  23364  nb3graprlem2  23365  cusgrarn  23372  cusgra1v  23374  cusgra2v  23375  nbcusgra  23376  cusgra3v  23377  usgrasscusgra  23396  uvtxel  23402  uvtxnbgra  23406  cusgrauvtxb  23409  constr2pth  23505  3v3e3cycl1  23535  constr3pthlem3  23548  4cycl4v4e  23557  4cycl4dv  23558  4cycl4dv4e  23559  esumpr2  26522  altopthsn  27997  wwlktovf  30256  wwlktovfo  30258  wrd2f1tovbij  30260  uvtxnb  30283  usgra2pthspth  30300  usgra2wlkspthlem1  30301  wwlkextfun  30366  wwlkextsur  30368  wwlkextbij  30370  usg2spthonot0  30413  clwlkisclwwlklem1  30454  frgraunss  30592  frgra1v  30595  frgra2v  30596  frgra3v  30599  1vwmgra  30600  3vfriswmgralem  30601  3vfriswmgra  30602  1to2vfriswmgra  30603  3cyclfrgrarn1  30609  4cycl2vnunb  30614  n4cyclfrgra  30615  vdn0frgrav2  30621  vdgn0frgrav2  30622  vdn1frgrav2  30623  vdgn1frgrav2  30624  frgrancvvdeqlem4  30631  frgrancvvdeqlemB  30636  frgrawopreglem5  30646  frgrawopreg2  30649  frg2woteqm  30657  usg2spot2nb  30663  numclwwlkovf2ex  30684  dihprrn  35076  dvh3dim  35096  mapdindp2  35371