Theorem preq2 4739

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

Syntax hints:   → wi 4   = wceq 1542  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-sn 4630  df-pr 4632

This theorem is referenced by:  preq12  4740  preq2i  4742  preq2d  4745  tpeq2  4748  ifpprsnss  4769  preq12bg  4855  prel12g  4865  elpreqprlem  4867  elpr2elpr  4870  opeq2  4875  uniprgOLD  4929  intprgOLD  4989  prex  5433  opth  5477  opeqsng  5504  propeqop  5508  relop  5851  funopg  6583  f1oprswap  6878  fprg  7153  fnprb  7210  fnpr2g  7212  pr2ne  9999  pr2neOLD  10000  prdom2  10001  dfac2b  10125  brdom7disj  10526  brdom6disj  10527  wunpr  10704  wunex2  10733  wuncval2  10742  grupr  10792  prunioo  13458  hashprg  14355  wwlktovf  14907  wwlktovfo  14909  wrd2f1tovbij  14911  joindef  18329  meetdef  18343  lspfixed  20741  hmphindis  23301  upgrex  28352  edglnl  28403  usgredg4  28474  usgredgreu  28475  uspgredg2vtxeu  28477  uspgredg2v  28481  nbgrel  28597  nbupgrel  28602  nbumgrvtx  28603  nbusgreledg  28610  nbgrnself  28616  nb3grprlem1  28637  nb3grprlem2  28638  uvtxel1  28653  uvtxusgrel  28660  cusgredg  28681  usgredgsscusgredg  28716  1egrvtxdg0  28768  ifpsnprss  28880  upgriswlk  28898  uspgrn2crct  29062  wwlksnextfun  29152  wwlksnextsurj  29154  wwlksnextbij  29156  clwlkclwwlklem2  29253  clwwlkinwwlk  29293  clwwlknonex2  29362  upgr1wlkdlem1  29398  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  eupth2lem3lem4  29484  frcond1  29519  frgr1v  29524  nfrgr2v  29525  frgr3v  29528  1vwmgr  29529  3vfriswmgrlem  29530  3vfriswmgr  29531  1to2vfriswmgr  29532  3cyclfrgrrn1  29538  4cycl2vnunb  29543  n4cyclfrgr  29544  vdgn1frgrv2  29549  frgrncvvdeqlem3  29554  frgrncvvdeqlem8  29559  frgrwopregbsn  29570  frgrwopreglem5ALT  29575  fusgr2wsp2nb  29587  esumpr2  33065  cplgredgex  34111  altopthsn  34933  dihprrn  40297  dvh3dim  40317  mapdindp2  40592  elsprel  46143  prelspr  46154  sprsymrelfolem2  46161  reupr  46190  reuopreuprim  46194  isomuspgrlem2d  46499  upgrwlkupwlk  46518  inlinecirc02plem  47472