Theorem preq2 4710

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

Syntax hints:   → wi 4   = wceq 1540  {cpr 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-un 3931  df-sn 4602  df-pr 4604

This theorem is referenced by:  preq12  4711  preq2i  4713  preq2d  4716  tpeq2  4719  ifpprsnss  4740  preq12bg  4829  prel12g  4840  elpreqprlem  4842  opeq2  4850  prex  5407  opth  5451  opeqsng  5478  propeqop  5482  relop  5830  funopg  6570  f1oprswap  6862  fprg  7145  fnprb  7200  fnpr2g  7202  prfi  9335  pr2ne  10018  pr2neOLD  10019  prdom2  10020  dfac2b  10145  brdom7disj  10545  brdom6disj  10546  wunpr  10723  wunex2  10752  wuncval2  10761  grupr  10811  prunioo  13498  hashprg  14413  wwlktovf  14975  wwlktovfo  14977  wrd2f1tovbij  14979  joindef  18386  meetdef  18400  lspfixed  21089  hmphindis  23735  upgrex  29071  edglnl  29122  usgredg4  29196  usgredgreu  29197  uspgredg2vtxeu  29199  uspgredg2v  29203  nbgrel  29319  nbupgrel  29324  nbumgrvtx  29325  nbusgreledg  29332  nbgrnself  29338  nb3grprlem1  29359  nb3grprlem2  29360  uvtxel1  29375  uvtxusgrel  29382  cusgredg  29403  usgredgsscusgredg  29439  1egrvtxdg0  29491  ifpsnprss  29603  upgriswlk  29621  uspgrn2crct  29790  wwlksnextfun  29880  wwlksnextsurj  29882  wwlksnextbij  29884  clwlkclwwlklem2  29981  clwwlkinwwlk  30021  clwwlknonex2  30090  upgr1wlkdlem1  30126  upgr3v3e3cycl  30161  upgr4cycl4dv4e  30166  eupth2lem3lem4  30212  frcond1  30247  frgr1v  30252  nfrgr2v  30253  frgr3v  30256  1vwmgr  30257  3vfriswmgrlem  30258  3vfriswmgr  30259  1to2vfriswmgr  30260  3cyclfrgrrn1  30266  4cycl2vnunb  30271  n4cyclfrgr  30272  vdgn1frgrv2  30277  frgrncvvdeqlem3  30282  frgrncvvdeqlem8  30287  frgrwopregbsn  30298  frgrwopreglem5ALT  30303  fusgr2wsp2nb  30315  esumpr2  34098  cplgredgex  35143  altopthsn  35979  dihprrn  41445  dvh3dim  41465  mapdindp2  41740  elsprel  47489  prelspr  47500  sprsymrelfolem2  47507  reupr  47536  reuopreuprim  47540  clnbgrel  47842  clnbupgrel  47848  sclnbgrel  47860  upgrimpths  47922  clnbgrgrim  47947  cycl3grtrilem  47958  cycl3grtri  47959  grimgrtri  47961  usgrgrtrirex  47962  stgr1  47973  stgrnbgr0  47976  isubgr3stgrlem4  47981  isubgr3stgrlem6  47983  grlimgrtri  48008  usgrexmpl1tri  48029  gpgnbgrvtx0  48076  gpgnbgrvtx1  48077  gpg5nbgrvtx03star  48082  gpg5nbgr3star  48083  gpg3kgrtriex  48091  upgrwlkupwlk  48115  inlinecirc02plem  48766