Theorem preq2 4738

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

Syntax hints:   → wi 4   = wceq 1536  {cpr 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-sn 4631  df-pr 4633

This theorem is referenced by:  preq12  4739  preq2i  4741  preq2d  4744  tpeq2  4747  ifpprsnss  4768  preq12bg  4857  prel12g  4868  elpreqprlem  4870  opeq2  4878  prex  5442  opth  5486  opeqsng  5512  propeqop  5516  relop  5863  funopg  6601  f1oprswap  6892  fprg  7174  fnprb  7227  fnpr2g  7229  prfi  9360  pr2ne  10041  pr2neOLD  10042  prdom2  10043  dfac2b  10168  brdom7disj  10568  brdom6disj  10569  wunpr  10746  wunex2  10775  wuncval2  10784  grupr  10834  prunioo  13517  hashprg  14430  wwlktovf  14991  wwlktovfo  14993  wrd2f1tovbij  14995  joindef  18433  meetdef  18447  lspfixed  21147  hmphindis  23820  upgrex  29123  edglnl  29174  usgredg4  29248  usgredgreu  29249  uspgredg2vtxeu  29251  uspgredg2v  29255  nbgrel  29371  nbupgrel  29376  nbumgrvtx  29377  nbusgreledg  29384  nbgrnself  29390  nb3grprlem1  29411  nb3grprlem2  29412  uvtxel1  29427  uvtxusgrel  29434  cusgredg  29455  usgredgsscusgredg  29491  1egrvtxdg0  29543  ifpsnprss  29655  upgriswlk  29673  uspgrn2crct  29837  wwlksnextfun  29927  wwlksnextsurj  29929  wwlksnextbij  29931  clwlkclwwlklem2  30028  clwwlkinwwlk  30068  clwwlknonex2  30137  upgr1wlkdlem1  30173  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eupth2lem3lem4  30259  frcond1  30294  frgr1v  30299  nfrgr2v  30300  frgr3v  30303  1vwmgr  30304  3vfriswmgrlem  30305  3vfriswmgr  30306  1to2vfriswmgr  30307  3cyclfrgrrn1  30313  4cycl2vnunb  30318  n4cyclfrgr  30319  vdgn1frgrv2  30324  frgrncvvdeqlem3  30329  frgrncvvdeqlem8  30334  frgrwopregbsn  30345  frgrwopreglem5ALT  30350  fusgr2wsp2nb  30362  esumpr2  34047  cplgredgex  35104  altopthsn  35942  dihprrn  41408  dvh3dim  41428  mapdindp2  41703  elsprel  47399  prelspr  47410  sprsymrelfolem2  47417  reupr  47446  reuopreuprim  47450  clnbgrel  47752  clnbupgrel  47758  sclnbgrel  47770  clnbgrgrim  47839  grimgrtri  47851  usgrgrtrirex  47852  stgr1  47863  stgrnbgr0  47866  isubgr3stgrlem4  47871  isubgr3stgrlem6  47873  grlimgrtri  47898  usgrexmpl1tri  47919  gpgnbgrvtx0  47964  gpgnbgrvtx1  47965  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  upgrwlkupwlk  47983  inlinecirc02plem  48635