Theorem preq2 4695

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  preq12  4696  preq2i  4698  preq2d  4701  tpeq2  4704  ifpprsnss  4725  preq12bg  4813  prel12g  4824  elpreqprlem  4826  opeq2  4834  prexOLD  5401  opth  5445  opeqsng  5475  propeqop  5479  relop  5828  funopg  6574  f1oprswap  6870  fprg  7159  fnprb  7214  fnpr2g  7216  prfi  9315  pr2ne  10084  prdom2  10085  dfac2b  10209  brdom7disj  10610  brdom6disj  10611  wunpr  10794  wunex2  10823  wuncval2  10832  grupr  10882  prunioo  13612  hashprg  14539  wwlktovf  15109  wwlktovfo  15111  wrd2f1tovbij  15113  joindef  18548  meetdef  18562  lspfixed  21406  hmphindis  24116  upgrex  29670  edglnl  29721  usgredg4  29798  usgredgreu  29799  uspgredg2vtxeu  29801  uspgredg2v  29805  nbgrel  29921  nbupgrel  29926  nbumgrvtx  29927  nbusgreledg  29934  nbgrnself  29940  nb3grprlem1  29961  nb3grprlem2  29962  uvtxel1  29977  uvtxusgrel  29984  cusgredg  30005  usgredgsscusgredg  30040  1egrvtxdg0  30092  ifpsnprss  30203  upgriswlk  30221  uspgrn2crct  30397  wwlksnextfun  30487  wwlksnextsurj  30489  wwlksnextbij  30491  clwlkclwwlklem2  30591  clwwlkinwwlk  30631  clwwlknonex2  30700  upgr1wlkdlem1  30736  upgr3v3e3cycl  30781  upgr4cycl4dv4e  30786  eupth2lem3lem4  30832  frcond1  30867  frgr1v  30872  nfrgr2v  30873  frgr3v  30876  1vwmgr  30877  3vfriswmgrlem  30878  3vfriswmgr  30879  1to2vfriswmgr  30880  3cyclfrgrrn1  30886  4cycl2vnunb  30891  n4cyclfrgr  30892  vdgn1frgrv2  30897  frgrncvvdeqlem3  30902  frgrncvvdeqlem8  30907  frgrwopregbsn  30918  frgrwopreglem5ALT  30923  fusgr2wsp2nb  30935  esumpr2  34699  cplgredgex  35905  altopthsn  36726  dihprrn  42484  dvh3dim  42504  mapdindp2  42779  elsprel  48557  prelspr  48568  sprsymrelfolem2  48575  reupr  48604  reuopreuprim  48608  clnbgrel  48926  clnbupgrel  48932  sclnbgrel  48945  upgrimpths  49007  clnbgrgrim  49032  cycl3grtrilem  49044  cycl3grtri  49045  grimgrtri  49047  usgrgrtrirex  49048  stgr1  49059  stgrnbgr0  49062  isubgr3stgrlem4  49067  isubgr3stgrlem6  49069  grlimgredgex  49098  grlimgrtri  49101  usgrexmpl1tri  49123  gpgnbgrvtx0  49172  gpgnbgrvtx1  49173  gpg5nbgrvtx03star  49178  gpg5nbgr3star  49179  gpg3kgrtriex  49187  pgnbgreunbgrlem1  49211  pgnbgreunbgrlem2lem1  49212  pgnbgreunbgrlem2lem2  49213  pgnbgreunbgrlem2lem3  49214  pgnbgreunbgrlem4  49217  pgnbgreunbgrlem5lem1  49218  pgnbgreunbgrlem5lem2  49219  pgnbgreunbgrlem5lem3  49220  pgnbgreunbgr  49223  grlimedgnedg  49229  upgrwlkupwlk  49238  inlinecirc02plem  49898