Theorem preq2 4678

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

Assertion

Ref	Expression
preq2	⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Proof of Theorem preq2

Step	Hyp	Ref	Expression
1		preq1 4677	. 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
2		prcom 4676	. 2 ⊢ {𝐶, 𝐴} = {𝐴, 𝐶}
3		prcom 4676	. 2 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
4	1, 2, 3	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1542  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-sn 4568  df-pr 4570

This theorem is referenced by:  preq12  4679  preq2i  4681  preq2d  4684  tpeq2  4687  ifpprsnss  4708  preq12bg  4796  prel12g  4807  elpreqprlem  4809  opeq2  4817  prexOLD  5385  opth  5429  opeqsng  5457  propeqop  5461  relop  5805  funopg  6532  f1oprswap  6825  fprg  7109  fnprb  7163  fnpr2g  7165  prfi  9234  pr2ne  9927  prdom2  9928  dfac2b  10053  brdom7disj  10453  brdom6disj  10454  wunpr  10632  wunex2  10661  wuncval2  10670  grupr  10720  prunioo  13434  hashprg  14357  wwlktovf  14918  wwlktovfo  14920  wrd2f1tovbij  14922  joindef  18340  meetdef  18354  lspfixed  21126  hmphindis  23762  upgrex  29161  edglnl  29212  usgredg4  29286  usgredgreu  29287  uspgredg2vtxeu  29289  uspgredg2v  29293  nbgrel  29409  nbupgrel  29414  nbumgrvtx  29415  nbusgreledg  29422  nbgrnself  29428  nb3grprlem1  29449  nb3grprlem2  29450  uvtxel1  29465  uvtxusgrel  29472  cusgredg  29493  usgredgsscusgredg  29528  1egrvtxdg0  29580  ifpsnprss  29691  upgriswlk  29709  uspgrn2crct  29876  wwlksnextfun  29966  wwlksnextsurj  29968  wwlksnextbij  29970  clwlkclwwlklem2  30070  clwwlkinwwlk  30110  clwwlknonex2  30179  upgr1wlkdlem1  30215  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eupth2lem3lem4  30301  frcond1  30336  frgr1v  30341  nfrgr2v  30342  frgr3v  30345  1vwmgr  30346  3vfriswmgrlem  30347  3vfriswmgr  30348  1to2vfriswmgr  30349  3cyclfrgrrn1  30355  4cycl2vnunb  30360  n4cyclfrgr  30361  vdgn1frgrv2  30366  frgrncvvdeqlem3  30371  frgrncvvdeqlem8  30376  frgrwopregbsn  30387  frgrwopreglem5ALT  30392  fusgr2wsp2nb  30404  esumpr2  34211  cplgredgex  35303  altopthsn  36143  dihprrn  41872  dvh3dim  41892  mapdindp2  42167  elsprel  47935  prelspr  47946  sprsymrelfolem2  47953  reupr  47982  reuopreuprim  47986  clnbgrel  48304  clnbupgrel  48310  sclnbgrel  48323  upgrimpths  48385  clnbgrgrim  48410  cycl3grtrilem  48422  cycl3grtri  48423  grimgrtri  48425  usgrgrtrirex  48426  stgr1  48437  stgrnbgr0  48440  isubgr3stgrlem4  48445  isubgr3stgrlem6  48447  grlimgredgex  48476  grlimgrtri  48479  usgrexmpl1tri  48501  gpgnbgrvtx0  48550  gpgnbgrvtx1  48551  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  gpg3kgrtriex  48565  pgnbgreunbgrlem1  48589  pgnbgreunbgrlem2lem1  48590  pgnbgreunbgrlem2lem2  48591  pgnbgreunbgrlem2lem3  48592  pgnbgreunbgrlem4  48595  pgnbgreunbgrlem5lem1  48596  pgnbgreunbgrlem5lem2  48597  pgnbgreunbgrlem5lem3  48598  pgnbgreunbgr  48601  grlimedgnedg  48607  upgrwlkupwlk  48616  inlinecirc02plem  49262