Theorem preq2 3943

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

Assertion

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

Proof of Theorem preq2

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

Syntax hints:   -> wi 4   = wceq 1362   {cpr 3867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-sn 3866  df-pr 3868

This theorem is referenced by:  preq12  3944  preq2i  3946  preq2d  3949  tpeq2  3952  preq12bg  4039  prel12g  4040  opeq2  4048  uniprg  4093  intprg  4150  prex  4522  opth  4554  opeqsn  4575  relop  4977  funopg  5438  f1oprswap  5668  fprg  5878  fnprb  5923  pr2ne  8160  prdom2  8161  dfac2  8288  brdom7disj  8686  brdom6disj  8687  wunpr  8863  wunex2  8892  wuncval2  8901  grupr  8951  prunioo  11400  hashprg  12138  isprm2lem  13752  joindef  15156  meetdef  15170  lspfixed  17130  hmphindis  19211  umgraex  23079  usgraedg4  23127  usgraedgreu  23128  nbgrael  23159  nbgraeledg  23163  nbgranself  23167  nbgraf1olem4  23175  nb3graprlem1  23181  nb3graprlem2  23182  cusgrarn  23189  cusgra1v  23191  cusgra2v  23192  nbcusgra  23193  cusgra3v  23194  usgrasscusgra  23213  uvtxel  23219  uvtxnbgra  23223  cusgrauvtxb  23226  constr2pth  23322  3v3e3cycl1  23352  constr3pthlem3  23365  4cycl4v4e  23374  4cycl4dv  23375  4cycl4dv4e  23376  esumpr2  26370  altopthsn  27838  wwlktovf  30094  wwlktovfo  30096  wrd2f1tovbij  30098  uvtxnb  30121  usgra2pthspth  30138  usgra2wlkspthlem1  30139  wwlkextfun  30204  wwlkextsur  30206  wwlkextbij  30208  usg2spthonot0  30251  clwlkisclwwlklem1  30292  frgraunss  30430  frgra1v  30433  frgra2v  30434  frgra3v  30437  1vwmgra  30438  3vfriswmgralem  30439  3vfriswmgra  30440  1to2vfriswmgra  30441  3cyclfrgrarn1  30447  4cycl2vnunb  30452  n4cyclfrgra  30453  vdn0frgrav2  30459  vdgn0frgrav2  30460  vdn1frgrav2  30461  vdgn1frgrav2  30462  frgrancvvdeqlem4  30469  frgrancvvdeqlemB  30474  frgrawopreglem5  30484  frgrawopreg2  30487  frg2woteqm  30495  usg2spot2nb  30501  numclwwlkovf2ex  30522  dihprrn  34641  dvh3dim  34661  mapdindp2  34936