Theorem preq2 4213

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 4212	. 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
2		prcom 4211	. 2 ⊢ {𝐶, 𝐴} = {𝐴, 𝐶}
3		prcom 4211	. 2 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
4	1, 2, 3	3eqtr4g 2669	1 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1475  {cpr 4127

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128

This theorem is referenced by:  preq12  4214  preq2i  4216  preq2d  4219  tpeq2  4222  preq12bg  4326  prel12g  4327  elpreqprlem  4333  elpr2elpr  4336  opeq2  4341  uniprg  4386  intprg  4446  prex  4836  opth  4871  opeqsn  4892  propeqop  4895  relop  5194  funopg  5836  f1oprswap  6092  fprg  6327  fnprb  6377  fnpr2g  6379  pr2ne  8711  prdom2  8712  dfac2  8836  brdom7disj  9234  brdom6disj  9235  wunpr  9410  wunex2  9439  wuncval2  9448  grupr  9498  prunioo  12172  hashprg  13043  hashprgOLD  13044  wwlktovf  13547  wwlktovfo  13549  wrd2f1tovbij  13551  isprm2lem  15232  joindef  16827  meetdef  16841  lspfixed  18949  hmphindis  21410  upgrex  25759  upgredg  25811  umgraex  25852  usgraedg4  25916  usgraedgreu  25917  nbgrael  25955  nbgraeledg  25959  nbgranself  25963  nbgraf1olem4  25973  nb3graprlem1  25980  nb3graprlem2  25981  cusgrarn  25988  cusgra1v  25990  cusgra2v  25991  nbcusgra  25992  cusgra3v  25993  usgrasscusgra  26011  uvtxel  26017  uvtxnbgra  26021  cusgrauvtxb  26024  uvtxnb  26025  constr2pth  26131  usgra2wlkspthlem1  26147  3v3e3cycl1  26172  constr3pthlem3  26185  4cycl4v4e  26194  4cycl4dv  26195  4cycl4dv4e  26196  wwlkextfun  26257  wwlkextsur  26259  wwlkextbij  26261  clwlkisclwwlklem1  26315  usg2spthonot0  26416  frgraunss  26522  frgra1v  26525  frgra2v  26526  frgra3v  26529  1vwmgra  26530  3vfriswmgralem  26531  3vfriswmgra  26532  1to2vfriswmgra  26533  3cyclfrgrarn1  26539  4cycl2vnunb  26544  n4cyclfrgra  26545  vdn0frgrav2  26550  vdgn0frgrav2  26551  vdn1frgrav2  26552  vdgn1frgrav2  26553  frgrancvvdeqlem4  26560  frgrancvvdeqlemB  26565  frgrawopreglem5  26575  frgrawopreg2  26578  frg2woteqm  26586  usg2spot2nb  26592  numclwwlkovf2ex  26613  esumpr2  29456  altopthsn  31238  dihprrn  35733  dvh3dim  35753  mapdindp2  36028  usgredg4  40444  usgredgreu  40445  uspgredg2vtxeu  40447  uspgredg2v  40451  nbgrel  40564  nbupgrel  40567  nbumgrvtx  40568  nbusgreledg  40575  nbgrnself  40583  nb3grprlem1  40608  nb3grprlem2  40609  uvtxael1  40622  uvtxusgrel  40630  cusgredg  40646  usgredgsscusgredg  40675  1egrvtxdg0  40727  1wlkvtxeledglem  40827  ifpprsnss  40845  upgr1wlkwlk  40847  uspgrn2crct  41011  wwlksnextfun  41104  wwlksnextsur  41106  wwlksnextbij  41108  clwlkclwwlklem2  41209  upgr11wlkdlem1  41312  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  eupth2lem3lem4  41399  frcond1  41438  frgr1v  41441  nfrgr2v  41442  frgr3v  41445  1vwmgr  41446  3vfriswmgrlem  41447  3vfriswmgr  41448  1to2vfriswmgr  41449  3cyclfrgrrn1  41455  4cycl2vnunb-av  41460  n4cyclfrgr  41461  vdgn1frgrv2  41466  frgrncvvdeqlem4  41472  frgrncvvdeqlemB  41477  frgrwopreglem5  41485  frgrwopreg2  41488  frgr2wwlkeqm  41496  fusgr2wsp2nb  41498  av-extwwlkfablem1  41508  av-numclwwlkovf2ex  41517