Theorem preq2 4065

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

Syntax hints:   -> wi 4   = wceq 1455   {cpr 3982

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-sn 3981  df-pr 3983

This theorem is referenced by:  preq12  4066  preq2i  4068  preq2d  4071  tpeq2  4074  preq12bg  4168  prel12g  4169  elpreqprlem  4174  opeq2  4181  uniprg  4226  intprg  4283  prex  4659  opth  4693  opeqsn  4714  relop  5007  funopg  5637  f1oprswap  5881  fprg  6102  fnprb  6152  fnpr2g  6154  pr2ne  8467  prdom2  8468  dfac2  8592  brdom7disj  8990  brdom6disj  8991  wunpr  9165  wunex2  9194  wuncval2  9203  grupr  9253  prunioo  11796  hashprg  12610  wwlktovf  13086  wwlktovfo  13088  wrd2f1tovbij  13090  isprm2lem  14686  joindef  16305  meetdef  16319  lspfixed  18406  hmphindis  20867  umgraex  25106  usgraedg4  25170  usgraedgreu  25171  nbgrael  25210  nbgraeledg  25214  nbgranself  25218  nbgraf1olem4  25228  nb3graprlem1  25235  nb3graprlem2  25236  cusgrarn  25243  cusgra1v  25245  cusgra2v  25246  nbcusgra  25247  cusgra3v  25248  usgrasscusgra  25267  uvtxel  25273  uvtxnbgra  25277  cusgrauvtxb  25280  uvtxnb  25281  constr2pth  25387  usgra2wlkspthlem1  25403  3v3e3cycl1  25428  constr3pthlem3  25441  4cycl4v4e  25450  4cycl4dv  25451  4cycl4dv4e  25452  wwlkextfun  25513  wwlkextsur  25515  wwlkextbij  25517  clwlkisclwwlklem1  25571  usg2spthonot0  25673  frgraunss  25779  frgra1v  25782  frgra2v  25783  frgra3v  25786  1vwmgra  25787  3vfriswmgralem  25788  3vfriswmgra  25789  1to2vfriswmgra  25790  3cyclfrgrarn1  25796  4cycl2vnunb  25801  n4cyclfrgra  25802  vdn0frgrav2  25807  vdgn0frgrav2  25808  vdn1frgrav2  25809  vdgn1frgrav2  25810  frgrancvvdeqlem4  25817  frgrancvvdeqlemB  25822  frgrawopreglem5  25832  frgrawopreg2  25835  frg2woteqm  25843  usg2spot2nb  25849  numclwwlkovf2ex  25870  esumpr2  28939  altopthsn  30778  dihprrn  35040  dvh3dim  35060  mapdindp2  35335  propeqop  39136  elpr2elpr  39140  upgrex  39327  upgredg  39372  usgredg4  39440  usgredgreu  39441  uspgredg2vtxeu  39443  uspgredg2v  39447  nbgrel  39556  nbupgrel  39559  nbumgrvtx  39560  nbusgreledg  39567  nbgrnself  39575  nb3grprlem1  39600  nb3grprlem2  39601  uvtxael1  39614  uvtxusgrel  39622  cusgredg  39638  usgredgsscusgredg  39666  1wlkvtxiedg  39783  wlk1wlk  39795  upgr1wlkwlk  39796  1wlkvtxeledg  39817  uspgrn2crct  39922  upgr11wlkdlem1  39956  upgr3v3e3cycl  40017  upgr4cycl4dv4e  40022  usgra2pthspth  40034  usgvincvad  40085  usgvincvadeu  40086  usgvincvadALT  40088  usgvincvadeuALT  40089