Theorem preq2 4688

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

Syntax hints:   → wi 4   = wceq 1541  {cpr 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-sn 4578  df-pr 4580

This theorem is referenced by:  preq12  4689  preq2i  4691  preq2d  4694  tpeq2  4697  ifpprsnss  4718  preq12bg  4806  prel12g  4817  elpreqprlem  4819  opeq2  4827  prex  5379  opth  5421  opeqsng  5448  propeqop  5452  relop  5796  funopg  6523  f1oprswap  6816  fprg  7097  fnprb  7151  fnpr2g  7153  prfi  9219  pr2ne  9907  prdom2  9908  dfac2b  10033  brdom7disj  10433  brdom6disj  10434  wunpr  10611  wunex2  10640  wuncval2  10649  grupr  10699  prunioo  13388  hashprg  14309  wwlktovf  14870  wwlktovfo  14872  wrd2f1tovbij  14874  joindef  18288  meetdef  18302  lspfixed  21074  hmphindis  23732  upgrex  29091  edglnl  29142  usgredg4  29216  usgredgreu  29217  uspgredg2vtxeu  29219  uspgredg2v  29223  nbgrel  29339  nbupgrel  29344  nbumgrvtx  29345  nbusgreledg  29352  nbgrnself  29358  nb3grprlem1  29379  nb3grprlem2  29380  uvtxel1  29395  uvtxusgrel  29402  cusgredg  29423  usgredgsscusgredg  29459  1egrvtxdg0  29511  ifpsnprss  29622  upgriswlk  29640  uspgrn2crct  29807  wwlksnextfun  29897  wwlksnextsurj  29899  wwlksnextbij  29901  clwlkclwwlklem2  30001  clwwlkinwwlk  30041  clwwlknonex2  30110  upgr1wlkdlem1  30146  upgr3v3e3cycl  30181  upgr4cycl4dv4e  30186  eupth2lem3lem4  30232  frcond1  30267  frgr1v  30272  nfrgr2v  30273  frgr3v  30276  1vwmgr  30277  3vfriswmgrlem  30278  3vfriswmgr  30279  1to2vfriswmgr  30280  3cyclfrgrrn1  30286  4cycl2vnunb  30291  n4cyclfrgr  30292  vdgn1frgrv2  30297  frgrncvvdeqlem3  30302  frgrncvvdeqlem8  30307  frgrwopregbsn  30318  frgrwopreglem5ALT  30323  fusgr2wsp2nb  30335  esumpr2  34152  cplgredgex  35237  altopthsn  36077  dihprrn  41598  dvh3dim  41618  mapdindp2  41893  elsprel  47637  prelspr  47648  sprsymrelfolem2  47655  reupr  47684  reuopreuprim  47688  clnbgrel  47990  clnbupgrel  47996  sclnbgrel  48009  upgrimpths  48071  clnbgrgrim  48096  cycl3grtrilem  48108  cycl3grtri  48109  grimgrtri  48111  usgrgrtrirex  48112  stgr1  48123  stgrnbgr0  48126  isubgr3stgrlem4  48131  isubgr3stgrlem6  48133  grlimgredgex  48162  grlimgrtri  48165  usgrexmpl1tri  48187  gpgnbgrvtx0  48236  gpgnbgrvtx1  48237  gpg5nbgrvtx03star  48242  gpg5nbgr3star  48243  gpg3kgrtriex  48251  pgnbgreunbgrlem1  48275  pgnbgreunbgrlem2lem1  48276  pgnbgreunbgrlem2lem2  48277  pgnbgreunbgrlem2lem3  48278  pgnbgreunbgrlem4  48281  pgnbgreunbgrlem5lem1  48282  pgnbgreunbgrlem5lem2  48283  pgnbgreunbgrlem5lem3  48284  pgnbgreunbgr  48287  grlimedgnedg  48293  upgrwlkupwlk  48302  inlinecirc02plem  48948