Theorem preq2 4700

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

Syntax hints:   → wi 4   = wceq 1541  {cpr 4593

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-un 3918  df-sn 4592  df-pr 4594

This theorem is referenced by:  preq12  4701  preq2i  4703  preq2d  4706  tpeq2  4709  ifpprsnss  4730  preq12bg  4816  prel12g  4826  elpreqprlem  4828  elpr2elpr  4831  opeq2  4836  uniprgOLD  4890  intprgOLD  4950  prex  5394  opth  5438  opeqsng  5465  propeqop  5469  relop  5811  funopg  6540  f1oprswap  6833  fprg  7106  fnprb  7163  fnpr2g  7165  pr2ne  9949  pr2neOLD  9950  prdom2  9951  dfac2b  10075  brdom7disj  10476  brdom6disj  10477  wunpr  10654  wunex2  10683  wuncval2  10692  grupr  10742  prunioo  13408  hashprg  14305  wwlktovf  14857  wwlktovfo  14859  wrd2f1tovbij  14861  joindef  18279  meetdef  18293  lspfixed  20648  hmphindis  23185  upgrex  28106  edglnl  28157  usgredg4  28228  usgredgreu  28229  uspgredg2vtxeu  28231  uspgredg2v  28235  nbgrel  28351  nbupgrel  28356  nbumgrvtx  28357  nbusgreledg  28364  nbgrnself  28370  nb3grprlem1  28391  nb3grprlem2  28392  uvtxel1  28407  uvtxusgrel  28414  cusgredg  28435  usgredgsscusgredg  28470  1egrvtxdg0  28522  ifpsnprss  28634  upgriswlk  28652  uspgrn2crct  28816  wwlksnextfun  28906  wwlksnextsurj  28908  wwlksnextbij  28910  clwlkclwwlklem2  29007  clwwlkinwwlk  29047  clwwlknonex2  29116  upgr1wlkdlem1  29152  upgr3v3e3cycl  29187  upgr4cycl4dv4e  29192  eupth2lem3lem4  29238  frcond1  29273  frgr1v  29278  nfrgr2v  29279  frgr3v  29282  1vwmgr  29283  3vfriswmgrlem  29284  3vfriswmgr  29285  1to2vfriswmgr  29286  3cyclfrgrrn1  29292  4cycl2vnunb  29297  n4cyclfrgr  29298  vdgn1frgrv2  29303  frgrncvvdeqlem3  29308  frgrncvvdeqlem8  29313  frgrwopregbsn  29324  frgrwopreglem5ALT  29329  fusgr2wsp2nb  29341  esumpr2  32755  cplgredgex  33801  altopthsn  34622  dihprrn  39962  dvh3dim  39982  mapdindp2  40257  elsprel  45787  prelspr  45798  sprsymrelfolem2  45805  reupr  45834  reuopreuprim  45838  isomuspgrlem2d  46143  upgrwlkupwlk  46162  inlinecirc02plem  46992