Theorem preq2 4667

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-sn 4559  df-pr 4561

This theorem is referenced by:  preq12  4668  preq2i  4670  preq2d  4673  tpeq2  4676  ifpprsnss  4697  preq12bg  4781  prel12g  4791  elpreqprlem  4793  elpr2elpr  4796  opeq2  4802  uniprgOLD  4856  intprgOLD  4912  prex  5350  opth  5385  opeqsng  5411  propeqop  5415  relop  5748  funopg  6452  f1oprswap  6743  fprg  7009  fnprb  7066  fnpr2g  7068  pr2ne  9692  prdom2  9693  dfac2b  9817  brdom7disj  10218  brdom6disj  10219  wunpr  10396  wunex2  10425  wuncval2  10434  grupr  10484  prunioo  13142  hashprg  14038  wwlktovf  14599  wwlktovfo  14601  wrd2f1tovbij  14603  joindef  18009  meetdef  18023  lspfixed  20305  hmphindis  22856  upgrex  27365  edglnl  27416  usgredg4  27487  usgredgreu  27488  uspgredg2vtxeu  27490  uspgredg2v  27494  nbgrel  27610  nbupgrel  27615  nbumgrvtx  27616  nbusgreledg  27623  nbgrnself  27629  nb3grprlem1  27650  nb3grprlem2  27651  uvtxel1  27666  uvtxusgrel  27673  cusgredg  27694  usgredgsscusgredg  27729  1egrvtxdg0  27781  ifpsnprss  27892  upgriswlk  27910  uspgrn2crct  28074  wwlksnextfun  28164  wwlksnextsurj  28166  wwlksnextbij  28168  clwlkclwwlklem2  28265  clwwlkinwwlk  28305  clwwlknonex2  28374  upgr1wlkdlem1  28410  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  eupth2lem3lem4  28496  frcond1  28531  frgr1v  28536  nfrgr2v  28537  frgr3v  28540  1vwmgr  28541  3vfriswmgrlem  28542  3vfriswmgr  28543  1to2vfriswmgr  28544  3cyclfrgrrn1  28550  4cycl2vnunb  28555  n4cyclfrgr  28556  vdgn1frgrv2  28561  frgrncvvdeqlem3  28566  frgrncvvdeqlem8  28571  frgrwopregbsn  28582  frgrwopreglem5ALT  28587  fusgr2wsp2nb  28599  esumpr2  31935  cplgredgex  32982  altopthsn  34190  dihprrn  39367  dvh3dim  39387  mapdindp2  39662  elsprel  44815  prelspr  44826  sprsymrelfolem2  44833  reupr  44862  reuopreuprim  44866  isomuspgrlem2d  45171  upgrwlkupwlk  45190  inlinecirc02plem  46020