Theorem preq2 4679

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

Syntax hints:   → wi 4   = wceq 1542  {cpr 4570

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-sn 4569  df-pr 4571

This theorem is referenced by:  preq12  4680  preq2i  4682  preq2d  4685  tpeq2  4688  ifpprsnss  4709  preq12bg  4797  prel12g  4808  elpreqprlem  4810  opeq2  4818  prexOLD  5378  opth  5422  opeqsng  5449  propeqop  5453  relop  5797  funopg  6524  f1oprswap  6817  fprg  7100  fnprb  7154  fnpr2g  7156  prfi  9225  pr2ne  9916  prdom2  9917  dfac2b  10042  brdom7disj  10442  brdom6disj  10443  wunpr  10621  wunex2  10650  wuncval2  10659  grupr  10709  prunioo  13423  hashprg  14346  wwlktovf  14907  wwlktovfo  14909  wrd2f1tovbij  14911  joindef  18329  meetdef  18343  lspfixed  21116  hmphindis  23771  upgrex  29180  edglnl  29231  usgredg4  29305  usgredgreu  29306  uspgredg2vtxeu  29308  uspgredg2v  29312  nbgrel  29428  nbupgrel  29433  nbumgrvtx  29434  nbusgreledg  29441  nbgrnself  29447  nb3grprlem1  29468  nb3grprlem2  29469  uvtxel1  29484  uvtxusgrel  29491  cusgredg  29512  usgredgsscusgredg  29548  1egrvtxdg0  29600  ifpsnprss  29711  upgriswlk  29729  uspgrn2crct  29896  wwlksnextfun  29986  wwlksnextsurj  29988  wwlksnextbij  29990  clwlkclwwlklem2  30090  clwwlkinwwlk  30130  clwwlknonex2  30199  upgr1wlkdlem1  30235  upgr3v3e3cycl  30270  upgr4cycl4dv4e  30275  eupth2lem3lem4  30321  frcond1  30356  frgr1v  30361  nfrgr2v  30362  frgr3v  30365  1vwmgr  30366  3vfriswmgrlem  30367  3vfriswmgr  30368  1to2vfriswmgr  30369  3cyclfrgrrn1  30375  4cycl2vnunb  30380  n4cyclfrgr  30381  vdgn1frgrv2  30386  frgrncvvdeqlem3  30391  frgrncvvdeqlem8  30396  frgrwopregbsn  30407  frgrwopreglem5ALT  30412  fusgr2wsp2nb  30424  esumpr2  34232  cplgredgex  35324  altopthsn  36164  dihprrn  41883  dvh3dim  41903  mapdindp2  42178  elsprel  47932  prelspr  47943  sprsymrelfolem2  47950  reupr  47979  reuopreuprim  47983  clnbgrel  48301  clnbupgrel  48307  sclnbgrel  48320  upgrimpths  48382  clnbgrgrim  48407  cycl3grtrilem  48419  cycl3grtri  48420  grimgrtri  48422  usgrgrtrirex  48423  stgr1  48434  stgrnbgr0  48437  isubgr3stgrlem4  48442  isubgr3stgrlem6  48444  grlimgredgex  48473  grlimgrtri  48476  usgrexmpl1tri  48498  gpgnbgrvtx0  48547  gpgnbgrvtx1  48548  gpg5nbgrvtx03star  48553  gpg5nbgr3star  48554  gpg3kgrtriex  48562  pgnbgreunbgrlem1  48586  pgnbgreunbgrlem2lem1  48587  pgnbgreunbgrlem2lem2  48588  pgnbgreunbgrlem2lem3  48589  pgnbgreunbgrlem4  48592  pgnbgreunbgrlem5lem1  48593  pgnbgreunbgrlem5lem2  48594  pgnbgreunbgrlem5lem3  48595  pgnbgreunbgr  48598  grlimedgnedg  48604  upgrwlkupwlk  48613  inlinecirc02plem  49259