Theorem preq2 4693

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

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

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 3444  df-un 3908  df-sn 4583  df-pr 4585

This theorem is referenced by:  preq12  4694  preq2i  4696  preq2d  4699  tpeq2  4702  ifpprsnss  4723  preq12bg  4811  prel12g  4822  elpreqprlem  4824  opeq2  4832  prexOLD  5389  opth  5432  opeqsng  5459  propeqop  5463  relop  5807  funopg  6534  f1oprswap  6827  fprg  7110  fnprb  7164  fnpr2g  7166  prfi  9236  pr2ne  9927  prdom2  9928  dfac2b  10053  brdom7disj  10453  brdom6disj  10454  wunpr  10632  wunex2  10661  wuncval2  10670  grupr  10720  prunioo  13409  hashprg  14330  wwlktovf  14891  wwlktovfo  14893  wrd2f1tovbij  14895  joindef  18309  meetdef  18323  lspfixed  21095  hmphindis  23753  upgrex  29177  edglnl  29228  usgredg4  29302  usgredgreu  29303  uspgredg2vtxeu  29305  uspgredg2v  29309  nbgrel  29425  nbupgrel  29430  nbumgrvtx  29431  nbusgreledg  29438  nbgrnself  29444  nb3grprlem1  29465  nb3grprlem2  29466  uvtxel1  29481  uvtxusgrel  29488  cusgredg  29509  usgredgsscusgredg  29545  1egrvtxdg0  29597  ifpsnprss  29708  upgriswlk  29726  uspgrn2crct  29893  wwlksnextfun  29983  wwlksnextsurj  29985  wwlksnextbij  29987  clwlkclwwlklem2  30087  clwwlkinwwlk  30127  clwwlknonex2  30196  upgr1wlkdlem1  30232  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  eupth2lem3lem4  30318  frcond1  30353  frgr1v  30358  nfrgr2v  30359  frgr3v  30362  1vwmgr  30363  3vfriswmgrlem  30364  3vfriswmgr  30365  1to2vfriswmgr  30366  3cyclfrgrrn1  30372  4cycl2vnunb  30377  n4cyclfrgr  30378  vdgn1frgrv2  30383  frgrncvvdeqlem3  30388  frgrncvvdeqlem8  30393  frgrwopregbsn  30404  frgrwopreglem5ALT  30409  fusgr2wsp2nb  30421  esumpr2  34244  cplgredgex  35334  altopthsn  36174  dihprrn  41799  dvh3dim  41819  mapdindp2  42094  elsprel  47832  prelspr  47843  sprsymrelfolem2  47850  reupr  47879  reuopreuprim  47883  clnbgrel  48185  clnbupgrel  48191  sclnbgrel  48204  upgrimpths  48266  clnbgrgrim  48291  cycl3grtrilem  48303  cycl3grtri  48304  grimgrtri  48306  usgrgrtrirex  48307  stgr1  48318  stgrnbgr0  48321  isubgr3stgrlem4  48326  isubgr3stgrlem6  48328  grlimgredgex  48357  grlimgrtri  48360  usgrexmpl1tri  48382  gpgnbgrvtx0  48431  gpgnbgrvtx1  48432  gpg5nbgrvtx03star  48437  gpg5nbgr3star  48438  gpg3kgrtriex  48446  pgnbgreunbgrlem1  48470  pgnbgreunbgrlem2lem1  48471  pgnbgreunbgrlem2lem2  48472  pgnbgreunbgrlem2lem3  48473  pgnbgreunbgrlem4  48476  pgnbgreunbgrlem5lem1  48477  pgnbgreunbgrlem5lem2  48478  pgnbgreunbgrlem5lem3  48479  pgnbgreunbgr  48482  grlimedgnedg  48488  upgrwlkupwlk  48497  inlinecirc02plem  49143