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 2829	1 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1567  {cpr 4593

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-sn 4592  df-pr 4594

This theorem is referenced by:  preq12  4703  preq2i  4705  preq2d  4708  tpeq2  4711  ifpprsnss  4732  preq12bg  4819  prel12g  4830  elpreqprlem  4832  opeq2  4840  prexOLD  5412  opth  5456  opeqsng  5484  propeqop  5488  relop  5834  funopg  6567  f1oprswap  6864  fprg  7150  fnprb  7204  fnpr2g  7206  prfi  9279  pr2ne  9985  prdom2  9986  dfac2b  10110  brdom7disj  10511  brdom6disj  10512  wunpr  10690  wunex2  10719  wuncval2  10728  grupr  10778  prunioo  13504  hashprg  14427  wwlktovf  14989  wwlktovfo  14991  wrd2f1tovbij  14993  joindef  18426  meetdef  18440  lspfixed  21226  hmphindis  23919  upgrex  29379  edglnl  29430  usgredg4  29504  usgredgreu  29505  uspgredg2vtxeu  29507  uspgredg2v  29511  nbgrel  29627  nbupgrel  29632  nbumgrvtx  29633  nbusgreledg  29640  nbgrnself  29646  nb3grprlem1  29667  nb3grprlem2  29668  uvtxel1  29683  uvtxusgrel  29690  cusgredg  29711  usgredgsscusgredg  29746  1egrvtxdg0  29798  ifpsnprss  29909  upgriswlk  29927  uspgrn2crct  30094  wwlksnextfun  30184  wwlksnextsurj  30186  wwlksnextbij  30188  clwlkclwwlklem2  30288  clwwlkinwwlk  30328  clwwlknonex2  30397  upgr1wlkdlem1  30433  upgr3v3e3cycl  30468  upgr4cycl4dv4e  30473  eupth2lem3lem4  30519  frcond1  30554  frgr1v  30559  nfrgr2v  30560  frgr3v  30563  1vwmgr  30564  3vfriswmgrlem  30565  3vfriswmgr  30566  1to2vfriswmgr  30567  3cyclfrgrrn1  30573  4cycl2vnunb  30578  n4cyclfrgr  30579  vdgn1frgrv2  30584  frgrncvvdeqlem3  30589  frgrncvvdeqlem8  30594  frgrwopregbsn  30605  frgrwopreglem5ALT  30610  fusgr2wsp2nb  30622  esumpr2  34398  cplgredgex  35508  altopthsn  36348  dihprrn  42085  dvh3dim  42105  mapdindp2  42380  elsprel  48106  prelspr  48117  sprsymrelfolem2  48124  reupr  48153  reuopreuprim  48157  clnbgrel  48475  clnbupgrel  48481  sclnbgrel  48494  upgrimpths  48556  clnbgrgrim  48581  cycl3grtrilem  48593  cycl3grtri  48594  grimgrtri  48596  usgrgrtrirex  48597  stgr1  48608  stgrnbgr0  48611  isubgr3stgrlem4  48616  isubgr3stgrlem6  48618  grlimgredgex  48647  grlimgrtri  48650  usgrexmpl1tri  48672  gpgnbgrvtx0  48721  gpgnbgrvtx1  48722  gpg5nbgrvtx03star  48727  gpg5nbgr3star  48728  gpg3kgrtriex  48736  pgnbgreunbgrlem1  48760  pgnbgreunbgrlem2lem1  48761  pgnbgreunbgrlem2lem2  48762  pgnbgreunbgrlem2lem3  48763  pgnbgreunbgrlem4  48766  pgnbgreunbgrlem5lem1  48767  pgnbgreunbgrlem5lem2  48768  pgnbgreunbgrlem5lem3  48769  pgnbgreunbgr  48772  grlimedgnedg  48778  upgrwlkupwlk  48787  inlinecirc02plem  49444