Theorem preq2 4734

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-sn 4627  df-pr 4629

This theorem is referenced by:  preq12  4735  preq2i  4737  preq2d  4740  tpeq2  4743  ifpprsnss  4764  preq12bg  4853  prel12g  4864  elpreqprlem  4866  opeq2  4874  prex  5437  opth  5481  opeqsng  5508  propeqop  5512  relop  5861  funopg  6600  f1oprswap  6892  fprg  7175  fnprb  7228  fnpr2g  7230  prfi  9363  pr2ne  10044  pr2neOLD  10045  prdom2  10046  dfac2b  10171  brdom7disj  10571  brdom6disj  10572  wunpr  10749  wunex2  10778  wuncval2  10787  grupr  10837  prunioo  13521  hashprg  14434  wwlktovf  14995  wwlktovfo  14997  wrd2f1tovbij  14999  joindef  18421  meetdef  18435  lspfixed  21130  hmphindis  23805  upgrex  29109  edglnl  29160  usgredg4  29234  usgredgreu  29235  uspgredg2vtxeu  29237  uspgredg2v  29241  nbgrel  29357  nbupgrel  29362  nbumgrvtx  29363  nbusgreledg  29370  nbgrnself  29376  nb3grprlem1  29397  nb3grprlem2  29398  uvtxel1  29413  uvtxusgrel  29420  cusgredg  29441  usgredgsscusgredg  29477  1egrvtxdg0  29529  ifpsnprss  29641  upgriswlk  29659  uspgrn2crct  29828  wwlksnextfun  29918  wwlksnextsurj  29920  wwlksnextbij  29922  clwlkclwwlklem2  30019  clwwlkinwwlk  30059  clwwlknonex2  30128  upgr1wlkdlem1  30164  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eupth2lem3lem4  30250  frcond1  30285  frgr1v  30290  nfrgr2v  30291  frgr3v  30294  1vwmgr  30295  3vfriswmgrlem  30296  3vfriswmgr  30297  1to2vfriswmgr  30298  3cyclfrgrrn1  30304  4cycl2vnunb  30309  n4cyclfrgr  30310  vdgn1frgrv2  30315  frgrncvvdeqlem3  30320  frgrncvvdeqlem8  30325  frgrwopregbsn  30336  frgrwopreglem5ALT  30341  fusgr2wsp2nb  30353  esumpr2  34068  cplgredgex  35126  altopthsn  35962  dihprrn  41428  dvh3dim  41448  mapdindp2  41723  elsprel  47462  prelspr  47473  sprsymrelfolem2  47480  reupr  47509  reuopreuprim  47513  clnbgrel  47815  clnbupgrel  47821  sclnbgrel  47833  clnbgrgrim  47902  cycl3grtrilem  47913  cycl3grtri  47914  grimgrtri  47916  usgrgrtrirex  47917  stgr1  47928  stgrnbgr0  47931  isubgr3stgrlem4  47936  isubgr3stgrlem6  47938  grlimgrtri  47963  usgrexmpl1tri  47984  gpgnbgrvtx0  48030  gpgnbgrvtx1  48031  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  gpg3kgrtriex  48045  upgrwlkupwlk  48056  inlinecirc02plem  48707