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  5380  opth  5424  opeqsng  5451  propeqop  5455  relop  5799  funopg  6526  f1oprswap  6819  fprg  7102  fnprb  7156  fnpr2g  7158  prfi  9227  pr2ne  9918  prdom2  9919  dfac2b  10044  brdom7disj  10444  brdom6disj  10445  wunpr  10623  wunex2  10652  wuncval2  10661  grupr  10711  prunioo  13425  hashprg  14348  wwlktovf  14909  wwlktovfo  14911  wrd2f1tovbij  14913  joindef  18331  meetdef  18345  lspfixed  21118  hmphindis  23772  upgrex  29175  edglnl  29226  usgredg4  29300  usgredgreu  29301  uspgredg2vtxeu  29303  uspgredg2v  29307  nbgrel  29423  nbupgrel  29428  nbumgrvtx  29429  nbusgreledg  29436  nbgrnself  29442  nb3grprlem1  29463  nb3grprlem2  29464  uvtxel1  29479  uvtxusgrel  29486  cusgredg  29507  usgredgsscusgredg  29543  1egrvtxdg0  29595  ifpsnprss  29706  upgriswlk  29724  uspgrn2crct  29891  wwlksnextfun  29981  wwlksnextsurj  29983  wwlksnextbij  29985  clwlkclwwlklem2  30085  clwwlkinwwlk  30125  clwwlknonex2  30194  upgr1wlkdlem1  30230  upgr3v3e3cycl  30265  upgr4cycl4dv4e  30270  eupth2lem3lem4  30316  frcond1  30351  frgr1v  30356  nfrgr2v  30357  frgr3v  30360  1vwmgr  30361  3vfriswmgrlem  30362  3vfriswmgr  30363  1to2vfriswmgr  30364  3cyclfrgrrn1  30370  4cycl2vnunb  30375  n4cyclfrgr  30376  vdgn1frgrv2  30381  frgrncvvdeqlem3  30386  frgrncvvdeqlem8  30391  frgrwopregbsn  30402  frgrwopreglem5ALT  30407  fusgr2wsp2nb  30419  esumpr2  34227  cplgredgex  35319  altopthsn  36159  dihprrn  41886  dvh3dim  41906  mapdindp2  42181  elsprel  47947  prelspr  47958  sprsymrelfolem2  47965  reupr  47994  reuopreuprim  47998  clnbgrel  48316  clnbupgrel  48322  sclnbgrel  48335  upgrimpths  48397  clnbgrgrim  48422  cycl3grtrilem  48434  cycl3grtri  48435  grimgrtri  48437  usgrgrtrirex  48438  stgr1  48449  stgrnbgr0  48452  isubgr3stgrlem4  48457  isubgr3stgrlem6  48459  grlimgredgex  48488  grlimgrtri  48491  usgrexmpl1tri  48513  gpgnbgrvtx0  48562  gpgnbgrvtx1  48563  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  gpg3kgrtriex  48577  pgnbgreunbgrlem1  48601  pgnbgreunbgrlem2lem1  48602  pgnbgreunbgrlem2lem2  48603  pgnbgreunbgrlem2lem3  48604  pgnbgreunbgrlem4  48607  pgnbgreunbgrlem5lem1  48608  pgnbgreunbgrlem5lem2  48609  pgnbgreunbgrlem5lem3  48610  pgnbgreunbgr  48613  grlimedgnedg  48619  upgrwlkupwlk  48628  inlinecirc02plem  49274