Theorem preq2 4671

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

Syntax hints:   → wi 4   = wceq 1539  {cpr 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-sn 4563  df-pr 4565

This theorem is referenced by:  preq12  4672  preq2i  4674  preq2d  4677  tpeq2  4680  ifpprsnss  4701  preq12bg  4785  prel12g  4795  elpreqprlem  4797  elpr2elpr  4800  opeq2  4806  uniprgOLD  4860  intprgOLD  4916  prex  5356  opth  5392  opeqsng  5418  propeqop  5422  relop  5762  funopg  6475  f1oprswap  6769  fprg  7036  fnprb  7093  fnpr2g  7095  pr2ne  9770  prdom2  9771  dfac2b  9895  brdom7disj  10296  brdom6disj  10297  wunpr  10474  wunex2  10503  wuncval2  10512  grupr  10562  prunioo  13222  hashprg  14119  wwlktovf  14680  wwlktovfo  14682  wrd2f1tovbij  14684  joindef  18103  meetdef  18117  lspfixed  20399  hmphindis  22957  upgrex  27471  edglnl  27522  usgredg4  27593  usgredgreu  27594  uspgredg2vtxeu  27596  uspgredg2v  27600  nbgrel  27716  nbupgrel  27721  nbumgrvtx  27722  nbusgreledg  27729  nbgrnself  27735  nb3grprlem1  27756  nb3grprlem2  27757  uvtxel1  27772  uvtxusgrel  27779  cusgredg  27800  usgredgsscusgredg  27835  1egrvtxdg0  27887  ifpsnprss  27999  upgriswlk  28017  uspgrn2crct  28182  wwlksnextfun  28272  wwlksnextsurj  28274  wwlksnextbij  28276  clwlkclwwlklem2  28373  clwwlkinwwlk  28413  clwwlknonex2  28482  upgr1wlkdlem1  28518  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  eupth2lem3lem4  28604  frcond1  28639  frgr1v  28644  nfrgr2v  28645  frgr3v  28648  1vwmgr  28649  3vfriswmgrlem  28650  3vfriswmgr  28651  1to2vfriswmgr  28652  3cyclfrgrrn1  28658  4cycl2vnunb  28663  n4cyclfrgr  28664  vdgn1frgrv2  28669  frgrncvvdeqlem3  28674  frgrncvvdeqlem8  28679  frgrwopregbsn  28690  frgrwopreglem5ALT  28695  fusgr2wsp2nb  28707  esumpr2  32044  cplgredgex  33091  altopthsn  34272  dihprrn  39447  dvh3dim  39467  mapdindp2  39742  elsprel  44938  prelspr  44949  sprsymrelfolem2  44956  reupr  44985  reuopreuprim  44989  isomuspgrlem2d  45294  upgrwlkupwlk  45313  inlinecirc02plem  46143