Theorem preq2 4701

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

Syntax hints:   → wi 4   = wceq 1570  {cpr 4592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3911  df-sn 4591  df-pr 4593

This theorem is referenced by:  preq12  4702  preq2i  4704  preq2d  4707  tpeq2  4710  ifpprsnss  4731  preq12bg  4819  prel12g  4830  elpreqprlem  4832  opeq2  4840  prexOLD  5416  opth  5460  opeqsng  5488  propeqop  5492  relop  5838  funopg  6572  f1oprswap  6868  fprg  7154  fnprb  7208  fnpr2g  7210  prfi  9284  pr2ne  9990  prdom2  9991  dfac2b  10115  brdom7disj  10516  brdom6disj  10517  wunpr  10695  wunex2  10724  wuncval2  10733  grupr  10783  prunioo  13509  hashprg  14433  wwlktovf  14995  wwlktovfo  14997  wrd2f1tovbij  14999  joindef  18431  meetdef  18445  lspfixed  21233  hmphindis  23935  upgrex  29423  edglnl  29474  usgredg4  29548  usgredgreu  29549  uspgredg2vtxeu  29551  uspgredg2v  29555  nbgrel  29671  nbupgrel  29676  nbumgrvtx  29677  nbusgreledg  29684  nbgrnself  29690  nb3grprlem1  29711  nb3grprlem2  29712  uvtxel1  29727  uvtxusgrel  29734  cusgredg  29755  usgredgsscusgredg  29790  1egrvtxdg0  29842  ifpsnprss  29953  upgriswlk  29971  uspgrn2crct  30138  wwlksnextfun  30228  wwlksnextsurj  30230  wwlksnextbij  30232  clwlkclwwlklem2  30332  clwwlkinwwlk  30372  clwwlknonex2  30441  upgr1wlkdlem1  30477  upgr3v3e3cycl  30512  upgr4cycl4dv4e  30517  eupth2lem3lem4  30563  frcond1  30598  frgr1v  30603  nfrgr2v  30604  frgr3v  30607  1vwmgr  30608  3vfriswmgrlem  30609  3vfriswmgr  30610  1to2vfriswmgr  30611  3cyclfrgrrn1  30617  4cycl2vnunb  30622  n4cyclfrgr  30623  vdgn1frgrv2  30628  frgrncvvdeqlem3  30633  frgrncvvdeqlem8  30638  frgrwopregbsn  30649  frgrwopreglem5ALT  30654  fusgr2wsp2nb  30666  esumpr2  34438  cplgredgex  35594  altopthsn  36434  dihprrn  42181  dvh3dim  42201  mapdindp2  42476  elsprel  48207  prelspr  48218  sprsymrelfolem2  48225  reupr  48254  reuopreuprim  48258  clnbgrel  48576  clnbupgrel  48582  sclnbgrel  48595  upgrimpths  48657  clnbgrgrim  48682  cycl3grtrilem  48694  cycl3grtri  48695  grimgrtri  48697  usgrgrtrirex  48698  stgr1  48709  stgrnbgr0  48712  isubgr3stgrlem4  48717  isubgr3stgrlem6  48719  grlimgredgex  48748  grlimgrtri  48751  usgrexmpl1tri  48773  gpgnbgrvtx0  48822  gpgnbgrvtx1  48823  gpg5nbgrvtx03star  48828  gpg5nbgr3star  48829  gpg3kgrtriex  48837  pgnbgreunbgrlem1  48861  pgnbgreunbgrlem2lem1  48862  pgnbgreunbgrlem2lem2  48863  pgnbgreunbgrlem2lem3  48864  pgnbgreunbgrlem4  48867  pgnbgreunbgrlem5lem1  48868  pgnbgreunbgrlem5lem2  48869  pgnbgreunbgrlem5lem3  48870  pgnbgreunbgr  48873  grlimedgnedg  48879  upgrwlkupwlk  48888  inlinecirc02plem  49549