Theorem preq2 4697

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-un 4154  df-sn 4589  df-pr 4591

This theorem is used by:  preq12  4698  preq2i  4700  preq2d  4703  tpeq2  4706  ifpprsnss  4727  preq12bg  4813  prel12g  4824  elpreqprlem  4826  opeq2  4846  prexOLD  5408  opth  5452  opeqsng  5482  propeqop  5486  relop  5838  funopg  6602  f1oprswap  6901  fprg  7191  fnprb  7245  fnpr2g  7247  prfi  9353  pr2ne  10123  prdom2  10124  dfac2b  10248  brdom7disj  10649  brdom6disj  10650  wunpr  10833  wunex2  10862  wuncval2  10871  grupr  10921  prunioo  13652  hashprg  14580  wwlktovf  15152  wwlktovfo  15154  wrd2f1tovbij  15156  joindef  18598  meetdef  18612  lspfixed  21457  hmphindis  24171  upgrex  29727  edglnl  29778  usgredg4  29855  usgredgreu  29856  uspgredg2vtxeu  29858  uspgredg2v  29862  nbgrel  29978  nbupgrel  29983  nbumgrvtx  29984  nbusgreledg  29991  nbgrnself  29997  nb3grprlem1  30018  nb3grprlem2  30019  uvtxel1  30034  uvtxusgrel  30041  cusgredg  30062  usgredgsscusgredg  30097  1egrvtxdg0  30149  ifpsnprss  30260  upgriswlk  30278  uspgrn2crct  30454  wwlksnextfun  30544  wwlksnextsurj  30546  wwlksnextbij  30548  clwlkclwwlklem2  30648  clwwlkinwwlk  30688  clwwlknonex2  30757  upgr1wlkdlem1  30793  upgr3v3e3cycl  30838  upgr4cycl4dv4e  30843  eupth2lem3lem4  30889  frcond1  30924  frgr1v  30929  nfrgr2v  30930  frgr3v  30933  1vwmgr  30934  3vfriswmgrlem  30935  3vfriswmgr  30936  1to2vfriswmgr  30937  3cyclfrgrrn1  30943  4cycl2vnunb  30948  n4cyclfrgr  30949  vdgn1frgrv2  30954  frgrncvvdeqlem3  30959  frgrncvvdeqlem8  30964  frgrwopregbsn  30975  frgrwopreglem5ALT  30980  fusgr2wsp2nb  30992  esumpr2  34810  gdlop1fv  36004  cplgredgex  36103  altopthsn  36941  dihprrn  42749  dvh3dim  42769  mapdindp2  43044  elsprel  48830  prelspr  48841  sprsymrelfolem2  48848  reupr  48877  reuopreuprim  48881  clnbgrel  49199  clnbupgrel  49205  sclnbgrel  49218  upgrimpths  49280  clnbgrgrim  49305  cycl3grtrilem  49317  cycl3grtri  49318  grimgrtri  49320  usgrgrtrirex  49321  stgr1  49332  stgrnbgr0  49335  isubgr3stgrlem4  49340  isubgr3stgrlem6  49342  grlimgredgex  49371  grlimgrtri  49374  usgrexmpl1tri  49396  gpgnbgrvtx0  49445  gpgnbgrvtx1  49446  gpg5nbgrvtx03star  49451  gpg5nbgr3star  49452  gpg3kgrtriex  49460  pgnbgreunbgrlem1  49484  pgnbgreunbgrlem2lem1  49485  pgnbgreunbgrlem2lem2  49486  pgnbgreunbgrlem2lem3  49487  pgnbgreunbgrlem4  49490  pgnbgreunbgrlem5lem1  49491  pgnbgreunbgrlem5lem2  49492  pgnbgreunbgrlem5lem3  49493  pgnbgreunbgr  49496  grlimedgnedg  49502  upgrwlkupwlk  49511  inlinecirc02plem  50229