MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  preq2 Structured version   Visualization version   GIF version

Theorem preq2 4471
Description: Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.)
Assertion
Ref Expression
preq2 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Proof of Theorem preq2
StepHypRef Expression
1 preq1 4470 . 2 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
2 prcom 4469 . 2 {𝐶, 𝐴} = {𝐴, 𝐶}
3 prcom 4469 . 2 {𝐶, 𝐵} = {𝐵, 𝐶}
41, 2, 33eqtr4g 2876 1 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  {cpr 4383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-un 3785  df-sn 4382  df-pr 4384
This theorem is referenced by:  preq12  4472  preq2i  4474  preq2d  4477  tpeq2  4480  ifpprsnss  4501  preq12bg  4584  prel12gOLD  4585  prel12g  4597  elpreqprlem  4599  elpr2elpr  4602  opeq2  4607  uniprg  4655  intprg  4714  prex  5112  opth  5147  opeqsng  5169  opeqsnOLD  5171  propeqop  5175  relop  5488  funopg  6145  f1oprswap  6406  fprg  6656  fnprb  6707  fnpr2g  6709  pr2ne  9121  prdom2  9122  dfac2b  9246  dfac2OLD  9248  brdom7disj  9648  brdom6disj  9649  wunpr  9826  wunex2  9855  wuncval2  9864  grupr  9914  prunioo  12544  hashprg  13420  wwlktovf  13944  wwlktovfo  13946  wrd2f1tovbij  13948  joindef  17229  meetdef  17243  lspfixed  19355  lspfixedOLD  19356  hmphindis  21835  upgrex  26224  edglnl  26276  usgredg4  26347  usgredgreu  26348  uspgredg2vtxeu  26350  uspgredg2v  26354  nbgrel  26472  nbgrelOLD  26473  nbupgrel  26480  nbumgrvtx  26481  nbusgreledg  26488  nbgrnself  26494  nb3grprlem1  26521  nb3grprlem2  26522  uvtxel1  26540  uvtxael1OLD  26542  uvtxusgrel  26549  cusgredg  26571  usgredgsscusgredg  26606  1egrvtxdg0  26658  ifpsnprss  26769  upgriswlk  26788  uspgrn2crct  26952  wwlksnextfun  27058  wwlksnextsur  27060  wwlksnextbij  27062  clwlkclwwlklem2  27166  clwwlkinwwlk  27212  clwwlknonex2  27301  upgr1wlkdlem1  27341  upgr3v3e3cycl  27376  upgr4cycl4dv4e  27381  eupth2lem3lem4  27427  frcond1  27464  frgr1v  27469  nfrgr2v  27470  frgr3v  27473  1vwmgr  27474  3vfriswmgrlem  27475  3vfriswmgr  27476  1to2vfriswmgr  27477  3cyclfrgrrn1  27483  4cycl2vnunb  27488  n4cyclfrgr  27489  vdgn1frgrv2  27494  frgrncvvdeqlem3  27499  frgrncvvdeqlem8  27504  frgrwopregbsn  27515  frgrwopreglem5ALT  27520  fusgr2wsp2nb  27532  esumpr2  30477  altopthsn  32411  dihprrn  37225  dvh3dim  37245  mapdindp2  37520  upgrwlkupwlk  42307  elsprel  42311  prelspr  42322  sprsymrelfolem2  42329
  Copyright terms: Public domain W3C validator