Theorem preq2 4688

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

Syntax hints:   → wi 4   = wceq 1540  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-sn 4580  df-pr 4582

This theorem is referenced by:  preq12  4689  preq2i  4691  preq2d  4694  tpeq2  4697  ifpprsnss  4718  preq12bg  4807  prel12g  4818  elpreqprlem  4820  opeq2  4828  prex  5379  opth  5423  opeqsng  5450  propeqop  5454  relop  5797  funopg  6520  f1oprswap  6812  fprg  7093  fnprb  7148  fnpr2g  7150  prfi  9232  pr2ne  9918  prdom2  9919  dfac2b  10044  brdom7disj  10444  brdom6disj  10445  wunpr  10622  wunex2  10651  wuncval2  10660  grupr  10710  prunioo  13402  hashprg  14320  wwlktovf  14881  wwlktovfo  14883  wrd2f1tovbij  14885  joindef  18298  meetdef  18312  lspfixed  21053  hmphindis  23700  upgrex  29055  edglnl  29106  usgredg4  29180  usgredgreu  29181  uspgredg2vtxeu  29183  uspgredg2v  29187  nbgrel  29303  nbupgrel  29308  nbumgrvtx  29309  nbusgreledg  29316  nbgrnself  29322  nb3grprlem1  29343  nb3grprlem2  29344  uvtxel1  29359  uvtxusgrel  29366  cusgredg  29387  usgredgsscusgredg  29423  1egrvtxdg0  29475  ifpsnprss  29586  upgriswlk  29604  uspgrn2crct  29771  wwlksnextfun  29861  wwlksnextsurj  29863  wwlksnextbij  29865  clwlkclwwlklem2  29962  clwwlkinwwlk  30002  clwwlknonex2  30071  upgr1wlkdlem1  30107  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eupth2lem3lem4  30193  frcond1  30228  frgr1v  30233  nfrgr2v  30234  frgr3v  30237  1vwmgr  30238  3vfriswmgrlem  30239  3vfriswmgr  30240  1to2vfriswmgr  30241  3cyclfrgrrn1  30247  4cycl2vnunb  30252  n4cyclfrgr  30253  vdgn1frgrv2  30258  frgrncvvdeqlem3  30263  frgrncvvdeqlem8  30268  frgrwopregbsn  30279  frgrwopreglem5ALT  30284  fusgr2wsp2nb  30296  esumpr2  34036  cplgredgex  35096  altopthsn  35937  dihprrn  41408  dvh3dim  41428  mapdindp2  41703  elsprel  47463  prelspr  47474  sprsymrelfolem2  47481  reupr  47510  reuopreuprim  47514  clnbgrel  47816  clnbupgrel  47822  sclnbgrel  47835  upgrimpths  47897  clnbgrgrim  47922  cycl3grtrilem  47934  cycl3grtri  47935  grimgrtri  47937  usgrgrtrirex  47938  stgr1  47949  stgrnbgr0  47952  isubgr3stgrlem4  47957  isubgr3stgrlem6  47959  grlimgredgex  47988  grlimgrtri  47991  usgrexmpl1tri  48013  gpgnbgrvtx0  48062  gpgnbgrvtx1  48063  gpg5nbgrvtx03star  48068  gpg5nbgr3star  48069  gpg3kgrtriex  48077  pgnbgreunbgrlem1  48101  pgnbgreunbgrlem2lem1  48102  pgnbgreunbgrlem2lem2  48103  pgnbgreunbgrlem2lem3  48104  pgnbgreunbgrlem4  48107  pgnbgreunbgrlem5lem1  48108  pgnbgreunbgrlem5lem2  48109  pgnbgreunbgrlem5lem3  48110  pgnbgreunbgr  48113  grlimedgnedg  48119  upgrwlkupwlk  48128  inlinecirc02plem  48775