Theorem preq2 4695

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-sn 4585  df-pr 4587

This theorem is used by:  preq12  4696  preq2i  4698  preq2d  4701  tpeq2  4704  ifpprsnss  4725  preq12bg  4813  prel12g  4824  elpreqprlem  4826  opeq2  4834  prexOLD  5408  opth  5452  opeqsng  5480  propeqop  5484  relop  5830  funopg  6567  f1oprswap  6863  fprg  7152  fnprb  7207  fnpr2g  7209  prfi  9293  pr2ne  10008  prdom2  10009  dfac2b  10133  brdom7disj  10534  brdom6disj  10535  wunpr  10718  wunex2  10747  wuncval2  10756  grupr  10806  prunioo  13534  hashprg  14459  wwlktovf  15029  wwlktovfo  15031  wrd2f1tovbij  15033  joindef  18462  meetdef  18476  lspfixed  21315  hmphindis  24023  upgrex  29549  edglnl  29600  usgredg4  29677  usgredgreu  29678  uspgredg2vtxeu  29680  uspgredg2v  29684  nbgrel  29800  nbupgrel  29805  nbumgrvtx  29806  nbusgreledg  29813  nbgrnself  29819  nb3grprlem1  29840  nb3grprlem2  29841  uvtxel1  29856  uvtxusgrel  29863  cusgredg  29884  usgredgsscusgredg  29919  1egrvtxdg0  29971  ifpsnprss  30082  upgriswlk  30100  uspgrn2crct  30276  wwlksnextfun  30366  wwlksnextsurj  30368  wwlksnextbij  30370  clwlkclwwlklem2  30470  clwwlkinwwlk  30510  clwwlknonex2  30579  upgr1wlkdlem1  30615  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  eupth2lem3lem4  30711  frcond1  30746  frgr1v  30751  nfrgr2v  30752  frgr3v  30755  1vwmgr  30756  3vfriswmgrlem  30757  3vfriswmgr  30758  1to2vfriswmgr  30759  3cyclfrgrrn1  30765  4cycl2vnunb  30770  n4cyclfrgr  30771  vdgn1frgrv2  30776  frgrncvvdeqlem3  30781  frgrncvvdeqlem8  30786  frgrwopregbsn  30797  frgrwopreglem5ALT  30802  fusgr2wsp2nb  30814  esumpr2  34577  cplgredgex  35719  altopthsn  36541  dihprrn  42299  dvh3dim  42319  mapdindp2  42594  elsprel  48375  prelspr  48386  sprsymrelfolem2  48393  reupr  48422  reuopreuprim  48426  clnbgrel  48744  clnbupgrel  48750  sclnbgrel  48763  upgrimpths  48825  clnbgrgrim  48850  cycl3grtrilem  48862  cycl3grtri  48863  grimgrtri  48865  usgrgrtrirex  48866  stgr1  48877  stgrnbgr0  48880  isubgr3stgrlem4  48885  isubgr3stgrlem6  48887  grlimgredgex  48916  grlimgrtri  48919  usgrexmpl1tri  48941  gpgnbgrvtx0  48990  gpgnbgrvtx1  48991  gpg5nbgrvtx03star  48996  gpg5nbgr3star  48997  gpg3kgrtriex  49005  pgnbgreunbgrlem1  49029  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  pgnbgreunbgrlem4  49035  pgnbgreunbgrlem5lem1  49036  pgnbgreunbgrlem5lem2  49037  pgnbgreunbgrlem5lem3  49038  pgnbgreunbgr  49041  grlimedgnedg  49047  upgrwlkupwlk  49056  inlinecirc02plem  49716