Theorem preq2 4112

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

Syntax hints:   -> wi 4   = wceq 1395   {cpr 4034

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-un 3476  df-sn 4033  df-pr 4035

This theorem is referenced by:  preq12  4113  preq2i  4115  preq2d  4118  tpeq2  4121  preq12bg  4211  prel12g  4212  opeq2  4220  uniprg  4265  intprg  4323  prex  4698  opth  4730  opeqsn  4752  relop  5163  funopg  5626  f1oprswap  5861  fprg  6081  fnprb  6131  pr2ne  8400  prdom2  8401  dfac2  8528  brdom7disj  8926  brdom6disj  8927  wunpr  9104  wunex2  9133  wuncval2  9142  grupr  9192  prunioo  11674  hashprg  12463  wwlktovf  12905  wwlktovfo  12907  wrd2f1tovbij  12909  isprm2lem  14235  joindef  15760  meetdef  15774  lspfixed  17900  hmphindis  20423  umgraex  24449  usgraedg4  24513  usgraedgreu  24514  nbgrael  24552  nbgraeledg  24556  nbgranself  24560  nbgraf1olem4  24570  nb3graprlem1  24577  nb3graprlem2  24578  cusgrarn  24585  cusgra1v  24587  cusgra2v  24588  nbcusgra  24589  cusgra3v  24590  usgrasscusgra  24609  uvtxel  24615  uvtxnbgra  24619  cusgrauvtxb  24622  uvtxnb  24623  constr2pth  24729  usgra2wlkspthlem1  24745  3v3e3cycl1  24770  constr3pthlem3  24783  4cycl4v4e  24792  4cycl4dv  24793  4cycl4dv4e  24794  wwlkextfun  24855  wwlkextsur  24857  wwlkextbij  24859  clwlkisclwwlklem1  24913  usg2spthonot0  25015  frgraunss  25121  frgra1v  25124  frgra2v  25125  frgra3v  25128  1vwmgra  25129  3vfriswmgralem  25130  3vfriswmgra  25131  1to2vfriswmgra  25132  3cyclfrgrarn1  25138  4cycl2vnunb  25143  n4cyclfrgra  25144  vdn0frgrav2  25149  vdgn0frgrav2  25150  vdn1frgrav2  25151  vdgn1frgrav2  25152  frgrancvvdeqlem4  25159  frgrancvvdeqlemB  25164  frgrawopreglem5  25174  frgrawopreg2  25177  frg2woteqm  25185  usg2spot2nb  25191  numclwwlkovf2ex  25212  esumpr2  28230  altopthsn  29773  usgra2pthspth  32571  usgvincvad  32624  usgvincvadeu  32625  usgvincvadALT  32627  usgvincvadeuALT  32628  dihprrn  37254  dvh3dim  37274  mapdindp2  37549