Theorem preq2 4682

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

Syntax hints:   → wi 4   = wceq 1541  {cpr 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-sn 4572  df-pr 4574

This theorem is referenced by:  preq12  4683  preq2i  4685  preq2d  4688  tpeq2  4691  ifpprsnss  4712  preq12bg  4800  prel12g  4811  elpreqprlem  4813  opeq2  4821  prex  5370  opth  5411  opeqsng  5438  propeqop  5442  relop  5785  funopg  6510  f1oprswap  6802  fprg  7083  fnprb  7137  fnpr2g  7139  prfi  9203  pr2ne  9891  prdom2  9892  dfac2b  10017  brdom7disj  10417  brdom6disj  10418  wunpr  10595  wunex2  10624  wuncval2  10633  grupr  10683  prunioo  13376  hashprg  14297  wwlktovf  14858  wwlktovfo  14860  wrd2f1tovbij  14862  joindef  18275  meetdef  18289  lspfixed  21060  hmphindis  23707  upgrex  29065  edglnl  29116  usgredg4  29190  usgredgreu  29191  uspgredg2vtxeu  29193  uspgredg2v  29197  nbgrel  29313  nbupgrel  29318  nbumgrvtx  29319  nbusgreledg  29326  nbgrnself  29332  nb3grprlem1  29353  nb3grprlem2  29354  uvtxel1  29369  uvtxusgrel  29376  cusgredg  29397  usgredgsscusgredg  29433  1egrvtxdg0  29485  ifpsnprss  29596  upgriswlk  29614  uspgrn2crct  29781  wwlksnextfun  29871  wwlksnextsurj  29873  wwlksnextbij  29875  clwlkclwwlklem2  29972  clwwlkinwwlk  30012  clwwlknonex2  30081  upgr1wlkdlem1  30117  upgr3v3e3cycl  30152  upgr4cycl4dv4e  30157  eupth2lem3lem4  30203  frcond1  30238  frgr1v  30243  nfrgr2v  30244  frgr3v  30247  1vwmgr  30248  3vfriswmgrlem  30249  3vfriswmgr  30250  1to2vfriswmgr  30251  3cyclfrgrrn1  30257  4cycl2vnunb  30262  n4cyclfrgr  30263  vdgn1frgrv2  30268  frgrncvvdeqlem3  30273  frgrncvvdeqlem8  30278  frgrwopregbsn  30289  frgrwopreglem5ALT  30294  fusgr2wsp2nb  30306  esumpr2  34072  cplgredgex  35157  altopthsn  35995  dihprrn  41465  dvh3dim  41485  mapdindp2  41760  elsprel  47506  prelspr  47517  sprsymrelfolem2  47524  reupr  47553  reuopreuprim  47557  clnbgrel  47859  clnbupgrel  47865  sclnbgrel  47878  upgrimpths  47940  clnbgrgrim  47965  cycl3grtrilem  47977  cycl3grtri  47978  grimgrtri  47980  usgrgrtrirex  47981  stgr1  47992  stgrnbgr0  47995  isubgr3stgrlem4  48000  isubgr3stgrlem6  48002  grlimgredgex  48031  grlimgrtri  48034  usgrexmpl1tri  48056  gpgnbgrvtx0  48105  gpgnbgrvtx1  48106  gpg5nbgrvtx03star  48111  gpg5nbgr3star  48112  gpg3kgrtriex  48120  pgnbgreunbgrlem1  48144  pgnbgreunbgrlem2lem1  48145  pgnbgreunbgrlem2lem2  48146  pgnbgreunbgrlem2lem3  48147  pgnbgreunbgrlem4  48150  pgnbgreunbgrlem5lem1  48151  pgnbgreunbgrlem5lem2  48152  pgnbgreunbgrlem5lem3  48153  pgnbgreunbgr  48156  grlimedgnedg  48162  upgrwlkupwlk  48171  inlinecirc02plem  48818