Theorem preq2 4080

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

Syntax hints:   -> wi 4   = wceq 1437   {cpr 4000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-un 3441  df-sn 3999  df-pr 4001

This theorem is referenced by:  preq12  4081  preq2i  4083  preq2d  4086  tpeq2  4089  preq12bg  4179  prel12g  4180  opeq2  4188  uniprg  4233  intprg  4290  prex  4663  opth  4695  opeqsn  4716  relop  5004  funopg  5633  f1oprswap  5871  fprg  6089  fnprb  6139  fnpr2g  6140  pr2ne  8445  prdom2  8446  dfac2  8569  brdom7disj  8967  brdom6disj  8968  wunpr  9142  wunex2  9171  wuncval2  9180  grupr  9230  prunioo  11769  hashprg  12579  wwlktovf  13032  wwlktovfo  13034  wrd2f1tovbij  13036  isprm2lem  14631  joindef  16250  meetdef  16264  lspfixed  18351  hmphindis  20811  umgraex  25049  usgraedg4  25113  usgraedgreu  25114  nbgrael  25153  nbgraeledg  25157  nbgranself  25161  nbgraf1olem4  25171  nb3graprlem1  25178  nb3graprlem2  25179  cusgrarn  25186  cusgra1v  25188  cusgra2v  25189  nbcusgra  25190  cusgra3v  25191  usgrasscusgra  25210  uvtxel  25216  uvtxnbgra  25220  cusgrauvtxb  25223  uvtxnb  25224  constr2pth  25330  usgra2wlkspthlem1  25346  3v3e3cycl1  25371  constr3pthlem3  25384  4cycl4v4e  25393  4cycl4dv  25394  4cycl4dv4e  25395  wwlkextfun  25456  wwlkextsur  25458  wwlkextbij  25460  clwlkisclwwlklem1  25514  usg2spthonot0  25616  frgraunss  25722  frgra1v  25725  frgra2v  25726  frgra3v  25729  1vwmgra  25730  3vfriswmgralem  25731  3vfriswmgra  25732  1to2vfriswmgra  25733  3cyclfrgrarn1  25739  4cycl2vnunb  25744  n4cyclfrgra  25745  vdn0frgrav2  25750  vdgn0frgrav2  25751  vdn1frgrav2  25752  vdgn1frgrav2  25753  frgrancvvdeqlem4  25760  frgrancvvdeqlemB  25765  frgrawopreglem5  25775  frgrawopreg2  25778  frg2woteqm  25786  usg2spot2nb  25792  numclwwlkovf2ex  25813  esumpr2  28897  altopthsn  30734  dihprrn  34964  dvh3dim  34984  mapdindp2  35259  propeqop  38866  upgrex  39016  upgredg  39048  usgredg4  39102  usgredgreu  39103  usgredg2vtxeu  39105  nbgrel  39204  nbupgrel  39207  nbumgrvtx  39208  nbusgreledg  39215  nbgrnself  39223  nb3grprlem1  39243  nb3grprlem2  39244  uvtxael1  39256  uvtxusgrel  39264  cusgredg  39278  usgredgsscusgredg  39306  usgra2pthspth  39314  usgvincvad  39365  usgvincvadeu  39366  usgvincvadALT  39368  usgvincvadeuALT  39369