Theorem preq2 4691

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 4151  df-sn 4585  df-pr 4587

This theorem is used by:  preq12  4692  preq2i  4694  preq2d  4697  tpeq2  4700  ifpprsnss  4721  preq12bg  4807  prel12g  4818  elpreqprlem  4820  opeq2  4840  prexOLD  5400  opth  5444  opeqsng  5474  propeqop  5478  relop  5827  funopg  6575  f1oprswap  6871  fprg  7160  fnprb  7215  fnpr2g  7217  prfi  9319  pr2ne  10088  prdom2  10089  dfac2b  10213  brdom7disj  10614  brdom6disj  10615  wunpr  10798  wunex2  10827  wuncval2  10836  grupr  10886  prunioo  13616  hashprg  14543  wwlktovf  15115  wwlktovfo  15117  wrd2f1tovbij  15119  joindef  18554  meetdef  18568  lspfixed  21412  hmphindis  24122  upgrex  29676  edglnl  29727  usgredg4  29804  usgredgreu  29805  uspgredg2vtxeu  29807  uspgredg2v  29811  nbgrel  29927  nbupgrel  29932  nbumgrvtx  29933  nbusgreledg  29940  nbgrnself  29946  nb3grprlem1  29967  nb3grprlem2  29968  uvtxel1  29983  uvtxusgrel  29990  cusgredg  30011  usgredgsscusgredg  30046  1egrvtxdg0  30098  ifpsnprss  30209  upgriswlk  30227  uspgrn2crct  30403  wwlksnextfun  30493  wwlksnextsurj  30495  wwlksnextbij  30497  clwlkclwwlklem2  30597  clwwlkinwwlk  30637  clwwlknonex2  30706  upgr1wlkdlem1  30742  upgr3v3e3cycl  30787  upgr4cycl4dv4e  30792  eupth2lem3lem4  30838  frcond1  30873  frgr1v  30878  nfrgr2v  30879  frgr3v  30882  1vwmgr  30883  3vfriswmgrlem  30884  3vfriswmgr  30885  1to2vfriswmgr  30886  3cyclfrgrrn1  30892  4cycl2vnunb  30897  n4cyclfrgr  30898  vdgn1frgrv2  30903  frgrncvvdeqlem3  30908  frgrncvvdeqlem8  30913  frgrwopregbsn  30924  frgrwopreglem5ALT  30929  fusgr2wsp2nb  30941  esumpr2  34746  cplgredgex  35982  altopthsn  36819  dihprrn  42577  dvh3dim  42597  mapdindp2  42872  elsprel  48651  prelspr  48662  sprsymrelfolem2  48669  reupr  48698  reuopreuprim  48702  clnbgrel  49020  clnbupgrel  49026  sclnbgrel  49039  upgrimpths  49101  clnbgrgrim  49126  cycl3grtrilem  49138  cycl3grtri  49139  grimgrtri  49141  usgrgrtrirex  49142  stgr1  49153  stgrnbgr0  49156  isubgr3stgrlem4  49161  isubgr3stgrlem6  49163  grlimgredgex  49192  grlimgrtri  49195  usgrexmpl1tri  49217  gpgnbgrvtx0  49266  gpgnbgrvtx1  49267  gpg5nbgrvtx03star  49272  gpg5nbgr3star  49273  gpg3kgrtriex  49281  pgnbgreunbgrlem1  49305  pgnbgreunbgrlem2lem1  49306  pgnbgreunbgrlem2lem2  49307  pgnbgreunbgrlem2lem3  49308  pgnbgreunbgrlem4  49311  pgnbgreunbgrlem5lem1  49312  pgnbgreunbgrlem5lem2  49313  pgnbgreunbgrlem5lem3  49314  pgnbgreunbgr  49317  grlimedgnedg  49323  upgrwlkupwlk  49332  inlinecirc02plem  49992