Theorem preq2 4673

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-un 3895  df-sn 4563  df-pr 4565

This theorem is referenced by:  preq12  4674  preq2i  4676  preq2d  4679  tpeq2  4682  ifpprsnss  4703  preq12bg  4791  prel12g  4802  elpreqprlem  4804  opeq2  4812  prexOLD  5379  opth  5423  opeqsng  5451  propeqop  5455  relop  5799  funopg  6526  f1oprswap  6819  fprg  7105  fnprb  7159  fnpr2g  7161  prfi  9231  pr2ne  9925  prdom2  9926  dfac2b  10051  brdom7disj  10451  brdom6disj  10452  wunpr  10630  wunex2  10659  wuncval2  10668  grupr  10718  prunioo  13432  hashprg  14355  wwlktovf  14916  wwlktovfo  14918  wrd2f1tovbij  14920  joindef  18338  meetdef  18352  lspfixed  21128  hmphindis  23787  upgrex  29186  edglnl  29237  usgredg4  29311  usgredgreu  29312  uspgredg2vtxeu  29314  uspgredg2v  29318  nbgrel  29434  nbupgrel  29439  nbumgrvtx  29440  nbusgreledg  29447  nbgrnself  29453  nb3grprlem1  29474  nb3grprlem2  29475  uvtxel1  29490  uvtxusgrel  29497  cusgredg  29518  usgredgsscusgredg  29553  1egrvtxdg0  29605  ifpsnprss  29716  upgriswlk  29734  uspgrn2crct  29901  wwlksnextfun  29991  wwlksnextsurj  29993  wwlksnextbij  29995  clwlkclwwlklem2  30095  clwwlkinwwlk  30135  clwwlknonex2  30204  upgr1wlkdlem1  30240  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  eupth2lem3lem4  30326  frcond1  30361  frgr1v  30366  nfrgr2v  30367  frgr3v  30370  1vwmgr  30371  3vfriswmgrlem  30372  3vfriswmgr  30373  1to2vfriswmgr  30374  3cyclfrgrrn1  30380  4cycl2vnunb  30385  n4cyclfrgr  30386  vdgn1frgrv2  30391  frgrncvvdeqlem3  30396  frgrncvvdeqlem8  30401  frgrwopregbsn  30412  frgrwopreglem5ALT  30417  fusgr2wsp2nb  30429  esumpr2  34258  cplgredgex  35356  altopthsn  36196  dihprrn  41925  dvh3dim  41945  mapdindp2  42220  elsprel  47957  prelspr  47968  sprsymrelfolem2  47975  reupr  48004  reuopreuprim  48008  clnbgrel  48326  clnbupgrel  48332  sclnbgrel  48345  upgrimpths  48407  clnbgrgrim  48432  cycl3grtrilem  48444  cycl3grtri  48445  grimgrtri  48447  usgrgrtrirex  48448  stgr1  48459  stgrnbgr0  48462  isubgr3stgrlem4  48467  isubgr3stgrlem6  48469  grlimgredgex  48498  grlimgrtri  48501  usgrexmpl1tri  48523  gpgnbgrvtx0  48572  gpgnbgrvtx1  48573  gpg5nbgrvtx03star  48578  gpg5nbgr3star  48579  gpg3kgrtriex  48587  pgnbgreunbgrlem1  48611  pgnbgreunbgrlem2lem1  48612  pgnbgreunbgrlem2lem2  48613  pgnbgreunbgrlem2lem3  48614  pgnbgreunbgrlem4  48617  pgnbgreunbgrlem5lem1  48618  pgnbgreunbgrlem5lem2  48619  pgnbgreunbgrlem5lem3  48620  pgnbgreunbgr  48623  grlimedgnedg  48629  upgrwlkupwlk  48638  inlinecirc02plem  49284