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  6572  f1oprswap  6868  fprg  7157  fnprb  7212  fnpr2g  7214  prfi  9308  pr2ne  10077  prdom2  10078  dfac2b  10202  brdom7disj  10603  brdom6disj  10604  wunpr  10787  wunex2  10816  wuncval2  10825  grupr  10875  prunioo  13605  hashprg  14532  wwlktovf  15102  wwlktovfo  15104  wrd2f1tovbij  15106  joindef  18541  meetdef  18555  lspfixed  21399  hmphindis  24109  upgrex  29663  edglnl  29714  usgredg4  29791  usgredgreu  29792  uspgredg2vtxeu  29794  uspgredg2v  29798  nbgrel  29914  nbupgrel  29919  nbumgrvtx  29920  nbusgreledg  29927  nbgrnself  29933  nb3grprlem1  29954  nb3grprlem2  29955  uvtxel1  29970  uvtxusgrel  29977  cusgredg  29998  usgredgsscusgredg  30033  1egrvtxdg0  30085  ifpsnprss  30196  upgriswlk  30214  uspgrn2crct  30390  wwlksnextfun  30480  wwlksnextsurj  30482  wwlksnextbij  30484  clwlkclwwlklem2  30584  clwwlkinwwlk  30624  clwwlknonex2  30693  upgr1wlkdlem1  30729  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  eupth2lem3lem4  30825  frcond1  30860  frgr1v  30865  nfrgr2v  30866  frgr3v  30869  1vwmgr  30870  3vfriswmgrlem  30871  3vfriswmgr  30872  1to2vfriswmgr  30873  3cyclfrgrrn1  30879  4cycl2vnunb  30884  n4cyclfrgr  30885  vdgn1frgrv2  30890  frgrncvvdeqlem3  30895  frgrncvvdeqlem8  30900  frgrwopregbsn  30911  frgrwopreglem5ALT  30916  fusgr2wsp2nb  30928  esumpr2  34692  cplgredgex  35884  altopthsn  36706  dihprrn  42463  dvh3dim  42483  mapdindp2  42758  elsprel  48526  prelspr  48537  sprsymrelfolem2  48544  reupr  48573  reuopreuprim  48577  clnbgrel  48895  clnbupgrel  48901  sclnbgrel  48914  upgrimpths  48976  clnbgrgrim  49001  cycl3grtrilem  49013  cycl3grtri  49014  grimgrtri  49016  usgrgrtrirex  49017  stgr1  49028  stgrnbgr0  49031  isubgr3stgrlem4  49036  isubgr3stgrlem6  49038  grlimgredgex  49067  grlimgrtri  49070  usgrexmpl1tri  49092  gpgnbgrvtx0  49141  gpgnbgrvtx1  49142  gpg5nbgrvtx03star  49147  gpg5nbgr3star  49148  gpg3kgrtriex  49156  pgnbgreunbgrlem1  49180  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  pgnbgreunbgrlem2lem3  49183  pgnbgreunbgrlem4  49186  pgnbgreunbgrlem5lem1  49187  pgnbgreunbgrlem5lem2  49188  pgnbgreunbgrlem5lem3  49189  pgnbgreunbgr  49192  grlimedgnedg  49198  upgrwlkupwlk  49207  inlinecirc02plem  49867