Theorem preq2 4701

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

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

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-sn 4593  df-pr 4595

This theorem is referenced by:  preq12  4702  preq2i  4704  preq2d  4707  tpeq2  4710  ifpprsnss  4731  preq12bg  4820  prel12g  4831  elpreqprlem  4833  opeq2  4841  prex  5395  opth  5439  opeqsng  5466  propeqop  5470  relop  5817  funopg  6553  f1oprswap  6847  fprg  7130  fnprb  7185  fnpr2g  7187  prfi  9281  pr2ne  9964  pr2neOLD  9965  prdom2  9966  dfac2b  10091  brdom7disj  10491  brdom6disj  10492  wunpr  10669  wunex2  10698  wuncval2  10707  grupr  10757  prunioo  13449  hashprg  14367  wwlktovf  14929  wwlktovfo  14931  wrd2f1tovbij  14933  joindef  18342  meetdef  18356  lspfixed  21045  hmphindis  23691  upgrex  29026  edglnl  29077  usgredg4  29151  usgredgreu  29152  uspgredg2vtxeu  29154  uspgredg2v  29158  nbgrel  29274  nbupgrel  29279  nbumgrvtx  29280  nbusgreledg  29287  nbgrnself  29293  nb3grprlem1  29314  nb3grprlem2  29315  uvtxel1  29330  uvtxusgrel  29337  cusgredg  29358  usgredgsscusgredg  29394  1egrvtxdg0  29446  ifpsnprss  29558  upgriswlk  29576  uspgrn2crct  29745  wwlksnextfun  29835  wwlksnextsurj  29837  wwlksnextbij  29839  clwlkclwwlklem2  29936  clwwlkinwwlk  29976  clwwlknonex2  30045  upgr1wlkdlem1  30081  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  eupth2lem3lem4  30167  frcond1  30202  frgr1v  30207  nfrgr2v  30208  frgr3v  30211  1vwmgr  30212  3vfriswmgrlem  30213  3vfriswmgr  30214  1to2vfriswmgr  30215  3cyclfrgrrn1  30221  4cycl2vnunb  30226  n4cyclfrgr  30227  vdgn1frgrv2  30232  frgrncvvdeqlem3  30237  frgrncvvdeqlem8  30242  frgrwopregbsn  30253  frgrwopreglem5ALT  30258  fusgr2wsp2nb  30270  esumpr2  34064  cplgredgex  35115  altopthsn  35956  dihprrn  41427  dvh3dim  41447  mapdindp2  41722  elsprel  47480  prelspr  47491  sprsymrelfolem2  47498  reupr  47527  reuopreuprim  47531  clnbgrel  47833  clnbupgrel  47839  sclnbgrel  47851  upgrimpths  47913  clnbgrgrim  47938  cycl3grtrilem  47949  cycl3grtri  47950  grimgrtri  47952  usgrgrtrirex  47953  stgr1  47964  stgrnbgr0  47967  isubgr3stgrlem4  47972  isubgr3stgrlem6  47974  grlimgrtri  47999  usgrexmpl1tri  48020  gpgnbgrvtx0  48069  gpgnbgrvtx1  48070  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  gpg3kgrtriex  48084  pgnbgreunbgrlem1  48107  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  pgnbgreunbgr  48119  upgrwlkupwlk  48132  inlinecirc02plem  48779