Theorem preq2 4107

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 4106	. 2 |- ( A = B -> { A , C } = { B , C } )
2		prcom 4105	. 2 |- { C , A } = { A , C }
3		prcom 4105	. 2 |- { C , B } = { B , C }
4	1, 2, 3	3eqtr4g 2533	1 |- ( A = B -> { C , A } = { C , B } )

Syntax hints:   -> wi 4   = wceq 1379   {cpr 4029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-sn 4028  df-pr 4030

This theorem is referenced by:  preq12  4108  preq2i  4110  preq2d  4113  tpeq2  4116  preq12bg  4205  prel12g  4206  opeq2  4214  uniprg  4259  intprg  4316  prex  4689  opth  4721  opeqsn  4743  relop  5151  funopg  5618  f1oprswap  5853  fprg  6068  fnprb  6117  pr2ne  8379  prdom2  8380  dfac2  8507  brdom7disj  8905  brdom6disj  8906  wunpr  9083  wunex2  9112  wuncval2  9121  grupr  9171  prunioo  11645  hashprg  12424  wwlktovf  12853  wwlktovfo  12855  wrd2f1tovbij  12857  isprm2lem  14079  joindef  15487  meetdef  15501  lspfixed  17557  hmphindis  20033  umgraex  23999  usgraedg4  24063  usgraedgreu  24064  nbgrael  24102  nbgraeledg  24106  nbgranself  24110  nbgraf1olem4  24120  nb3graprlem1  24127  nb3graprlem2  24128  cusgrarn  24135  cusgra1v  24137  cusgra2v  24138  nbcusgra  24139  cusgra3v  24140  usgrasscusgra  24159  uvtxel  24165  uvtxnbgra  24169  cusgrauvtxb  24172  uvtxnb  24173  constr2pth  24279  usgra2wlkspthlem1  24295  3v3e3cycl1  24320  constr3pthlem3  24333  4cycl4v4e  24342  4cycl4dv  24343  4cycl4dv4e  24344  wwlkextfun  24405  wwlkextsur  24407  wwlkextbij  24409  clwlkisclwwlklem1  24463  usg2spthonot0  24565  frgraunss  24671  frgra1v  24674  frgra2v  24675  frgra3v  24678  1vwmgra  24679  3vfriswmgralem  24680  3vfriswmgra  24681  1to2vfriswmgra  24682  3cyclfrgrarn1  24688  4cycl2vnunb  24693  n4cyclfrgra  24694  vdn0frgrav2  24700  vdgn0frgrav2  24701  vdn1frgrav2  24702  vdgn1frgrav2  24703  frgrancvvdeqlem4  24710  frgrancvvdeqlemB  24715  frgrawopreglem5  24725  frgrawopreg2  24728  frg2woteqm  24736  usg2spot2nb  24742  numclwwlkovf2ex  24763  esumpr2  27714  altopthsn  29188  usgra2pthspth  31820  usgvincvad  31873  usgvincvadeu  31874  usgvincvadALT  31876  usgvincvadeuALT  31877  dihprrn  36223  dvh3dim  36243  mapdindp2  36518