Theorem preq2 4702

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

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

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-sn 4592  df-pr 4594

This theorem is used by:  preq12  4703  preq2i  4705  preq2d  4708  tpeq2  4711  ifpprsnss  4732  preq12bg  4820  prel12g  4831  elpreqprlem  4833  opeq2  4841  prexOLD  5416  opth  5460  opeqsng  5488  propeqop  5492  relop  5838  funopg  6574  f1oprswap  6870  fprg  7156  fnprb  7210  fnpr2g  7212  prfi  9286  pr2ne  10001  prdom2  10002  dfac2b  10126  brdom7disj  10526  brdom6disj  10527  wunpr  10705  wunex2  10734  wuncval2  10743  grupr  10793  prunioo  13519  hashprg  14444  wwlktovf  15012  wwlktovfo  15014  wrd2f1tovbij  15016  joindef  18447  meetdef  18461  lspfixed  21281  hmphindis  23983  upgrex  29471  edglnl  29522  usgredg4  29596  usgredgreu  29597  uspgredg2vtxeu  29599  uspgredg2v  29603  nbgrel  29719  nbupgrel  29724  nbumgrvtx  29725  nbusgreledg  29732  nbgrnself  29738  nb3grprlem1  29759  nb3grprlem2  29760  uvtxel1  29775  uvtxusgrel  29782  cusgredg  29803  usgredgsscusgredg  29838  1egrvtxdg0  29890  ifpsnprss  30001  upgriswlk  30019  uspgrn2crct  30186  wwlksnextfun  30276  wwlksnextsurj  30278  wwlksnextbij  30280  clwlkclwwlklem2  30380  clwwlkinwwlk  30420  clwwlknonex2  30489  upgr1wlkdlem1  30525  upgr3v3e3cycl  30560  upgr4cycl4dv4e  30565  eupth2lem3lem4  30611  frcond1  30646  frgr1v  30651  nfrgr2v  30652  frgr3v  30655  1vwmgr  30656  3vfriswmgrlem  30657  3vfriswmgr  30658  1to2vfriswmgr  30659  3cyclfrgrrn1  30665  4cycl2vnunb  30670  n4cyclfrgr  30671  vdgn1frgrv2  30676  frgrncvvdeqlem3  30681  frgrncvvdeqlem8  30686  frgrwopregbsn  30697  frgrwopreglem5ALT  30702  fusgr2wsp2nb  30714  esumpr2  34480  cplgredgex  35626  altopthsn  36466  dihprrn  42233  dvh3dim  42253  mapdindp2  42528  elsprel  48257  prelspr  48268  sprsymrelfolem2  48275  reupr  48304  reuopreuprim  48308  clnbgrel  48626  clnbupgrel  48632  sclnbgrel  48645  upgrimpths  48707  clnbgrgrim  48732  cycl3grtrilem  48744  cycl3grtri  48745  grimgrtri  48747  usgrgrtrirex  48748  stgr1  48759  stgrnbgr0  48762  isubgr3stgrlem4  48767  isubgr3stgrlem6  48769  grlimgredgex  48798  grlimgrtri  48801  usgrexmpl1tri  48823  gpgnbgrvtx0  48872  gpgnbgrvtx1  48873  gpg5nbgrvtx03star  48878  gpg5nbgr3star  48879  gpg3kgrtriex  48887  pgnbgreunbgrlem1  48911  pgnbgreunbgrlem2lem1  48912  pgnbgreunbgrlem2lem2  48913  pgnbgreunbgrlem2lem3  48914  pgnbgreunbgrlem4  48917  pgnbgreunbgrlem5lem1  48918  pgnbgreunbgrlem5lem2  48919  pgnbgreunbgrlem5lem3  48920  pgnbgreunbgr  48923  grlimedgnedg  48929  upgrwlkupwlk  48938  inlinecirc02plem  49599