Theorem preq2 4690

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

Syntax hints:   → wi 4   = wceq 1559  {cpr 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-sn 4580  df-pr 4582

This theorem is referenced by:  preq12  4691  preq2i  4693  preq2d  4696  tpeq2  4699  ifpprsnss  4720  preq12bg  4808  prel12g  4819  elpreqprlem  4821  opeq2  4829  prexOLD  5397  opth  5441  opeqsng  5469  propeqop  5473  relop  5818  funopg  6550  f1oprswap  6847  fprg  7133  fnprb  7187  fnpr2g  7189  prfi  9262  pr2ne  9955  prdom2  9956  dfac2b  10081  brdom7disj  10482  brdom6disj  10483  wunpr  10661  wunex2  10690  wuncval2  10699  grupr  10749  prunioo  13479  hashprg  14402  wwlktovf  14963  wwlktovfo  14965  wrd2f1tovbij  14967  joindef  18397  meetdef  18411  lspfixed  21186  hmphindis  23845  upgrex  29250  edglnl  29301  usgredg4  29375  usgredgreu  29376  uspgredg2vtxeu  29378  uspgredg2v  29382  nbgrel  29498  nbupgrel  29503  nbumgrvtx  29504  nbusgreledg  29511  nbgrnself  29517  nb3grprlem1  29538  nb3grprlem2  29539  uvtxel1  29554  uvtxusgrel  29561  cusgredg  29582  usgredgsscusgredg  29617  1egrvtxdg0  29669  ifpsnprss  29780  upgriswlk  29798  uspgrn2crct  29965  wwlksnextfun  30055  wwlksnextsurj  30057  wwlksnextbij  30059  clwlkclwwlklem2  30159  clwwlkinwwlk  30199  clwwlknonex2  30268  upgr1wlkdlem1  30304  upgr3v3e3cycl  30339  upgr4cycl4dv4e  30344  eupth2lem3lem4  30390  frcond1  30425  frgr1v  30430  nfrgr2v  30431  frgr3v  30434  1vwmgr  30435  3vfriswmgrlem  30436  3vfriswmgr  30437  1to2vfriswmgr  30438  3cyclfrgrrn1  30444  4cycl2vnunb  30449  n4cyclfrgr  30450  vdgn1frgrv2  30455  frgrncvvdeqlem3  30460  frgrncvvdeqlem8  30465  frgrwopregbsn  30476  frgrwopreglem5ALT  30481  fusgr2wsp2nb  30493  esumpr2  34325  cplgredgex  35432  altopthsn  36272  dihprrn  42011  dvh3dim  42031  mapdindp2  42306  elsprel  48042  prelspr  48053  sprsymrelfolem2  48060  reupr  48089  reuopreuprim  48093  clnbgrel  48411  clnbupgrel  48417  sclnbgrel  48430  upgrimpths  48492  clnbgrgrim  48517  cycl3grtrilem  48529  cycl3grtri  48530  grimgrtri  48532  usgrgrtrirex  48533  stgr1  48544  stgrnbgr0  48547  isubgr3stgrlem4  48552  isubgr3stgrlem6  48554  grlimgredgex  48583  grlimgrtri  48586  usgrexmpl1tri  48608  gpgnbgrvtx0  48657  gpgnbgrvtx1  48658  gpg5nbgrvtx03star  48663  gpg5nbgr3star  48664  gpg3kgrtriex  48672  pgnbgreunbgrlem1  48696  pgnbgreunbgrlem2lem1  48697  pgnbgreunbgrlem2lem2  48698  pgnbgreunbgrlem2lem3  48699  pgnbgreunbgrlem4  48702  pgnbgreunbgrlem5lem1  48703  pgnbgreunbgrlem5lem2  48704  pgnbgreunbgrlem5lem3  48705  pgnbgreunbgr  48708  grlimedgnedg  48714  upgrwlkupwlk  48723  inlinecirc02plem  49369