Theorem preq2 4691

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-sn 4581  df-pr 4583

This theorem is referenced by:  preq12  4692  preq2i  4694  preq2d  4697  tpeq2  4700  ifpprsnss  4721  preq12bg  4809  prel12g  4820  elpreqprlem  4822  opeq2  4830  prex  5382  opth  5424  opeqsng  5451  propeqop  5455  relop  5799  funopg  6526  f1oprswap  6819  fprg  7100  fnprb  7154  fnpr2g  7156  prfi  9224  pr2ne  9915  prdom2  9916  dfac2b  10041  brdom7disj  10441  brdom6disj  10442  wunpr  10620  wunex2  10649  wuncval2  10658  grupr  10708  prunioo  13397  hashprg  14318  wwlktovf  14879  wwlktovfo  14881  wrd2f1tovbij  14883  joindef  18297  meetdef  18311  lspfixed  21083  hmphindis  23741  upgrex  29165  edglnl  29216  usgredg4  29290  usgredgreu  29291  uspgredg2vtxeu  29293  uspgredg2v  29297  nbgrel  29413  nbupgrel  29418  nbumgrvtx  29419  nbusgreledg  29426  nbgrnself  29432  nb3grprlem1  29453  nb3grprlem2  29454  uvtxel1  29469  uvtxusgrel  29476  cusgredg  29497  usgredgsscusgredg  29533  1egrvtxdg0  29585  ifpsnprss  29696  upgriswlk  29714  uspgrn2crct  29881  wwlksnextfun  29971  wwlksnextsurj  29973  wwlksnextbij  29975  clwlkclwwlklem2  30075  clwwlkinwwlk  30115  clwwlknonex2  30184  upgr1wlkdlem1  30220  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  eupth2lem3lem4  30306  frcond1  30341  frgr1v  30346  nfrgr2v  30347  frgr3v  30350  1vwmgr  30351  3vfriswmgrlem  30352  3vfriswmgr  30353  1to2vfriswmgr  30354  3cyclfrgrrn1  30360  4cycl2vnunb  30365  n4cyclfrgr  30366  vdgn1frgrv2  30371  frgrncvvdeqlem3  30376  frgrncvvdeqlem8  30381  frgrwopregbsn  30392  frgrwopreglem5ALT  30397  fusgr2wsp2nb  30409  esumpr2  34224  cplgredgex  35315  altopthsn  36155  dihprrn  41686  dvh3dim  41706  mapdindp2  41981  elsprel  47721  prelspr  47732  sprsymrelfolem2  47739  reupr  47768  reuopreuprim  47772  clnbgrel  48074  clnbupgrel  48080  sclnbgrel  48093  upgrimpths  48155  clnbgrgrim  48180  cycl3grtrilem  48192  cycl3grtri  48193  grimgrtri  48195  usgrgrtrirex  48196  stgr1  48207  stgrnbgr0  48210  isubgr3stgrlem4  48215  isubgr3stgrlem6  48217  grlimgredgex  48246  grlimgrtri  48249  usgrexmpl1tri  48271  gpgnbgrvtx0  48320  gpgnbgrvtx1  48321  gpg5nbgrvtx03star  48326  gpg5nbgr3star  48327  gpg3kgrtriex  48335  pgnbgreunbgrlem1  48359  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5lem1  48366  pgnbgreunbgrlem5lem2  48367  pgnbgreunbgrlem5lem3  48368  pgnbgreunbgr  48371  grlimedgnedg  48377  upgrwlkupwlk  48386  inlinecirc02plem  49032