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

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

Proof of Theorem preq2
StepHypRef Expression
1 preq1 4410 . 2 (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
2 prcom 4409 . 2 {𝐶, 𝐴} = {𝐴, 𝐶}
3 prcom 4409 . 2 {𝐶, 𝐵} = {𝐵, 𝐶}
41, 2, 33eqtr4g 2817 1 (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  {cpr 4321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-un 3718  df-sn 4320  df-pr 4322
This theorem is referenced by:  preq12  4412  preq2i  4414  preq2d  4417  tpeq2  4420  ifpprsnss  4441  preq12bg  4528  prel12gOLD  4529  prel12g  4542  elpreqprlem  4544  elpr2elpr  4547  opeq2  4552  uniprg  4600  intprg  4661  prex  5056  opth  5091  opeqsn  5113  propeqop  5116  relop  5426  funopg  6081  f1oprswap  6339  fprg  6583  fnprb  6634  fnpr2g  6636  pr2ne  9016  prdom2  9017  dfac2b  9141  dfac2OLD  9143  brdom7disj  9543  brdom6disj  9544  wunpr  9721  wunex2  9750  wuncval2  9759  grupr  9809  prunioo  12492  hashprg  13372  hashprgOLD  13373  wwlktovf  13898  wwlktovfo  13900  wrd2f1tovbij  13902  joindef  17203  meetdef  17217  lspfixed  19328  hmphindis  21800  upgrex  26184  edglnl  26235  usgredg4  26306  usgredgreu  26307  uspgredg2vtxeu  26309  uspgredg2v  26313  nbgrel  26430  nbgrelOLD  26431  nbupgrel  26438  nbumgrvtx  26439  nbusgreledg  26446  nbgrnself  26452  nb3grprlem1  26478  nb3grprlem2  26479  uvtxel1  26497  uvtxael1OLD  26499  uvtxusgrel  26506  cusgredg  26528  usgredgsscusgredg  26563  1egrvtxdg0  26615  ifpsnprss  26726  upgriswlk  26745  uspgrn2crct  26909  wwlksnextfun  27014  wwlksnextsur  27016  wwlksnextbij  27018  clwlkclwwlklem2  27121  clwwlkinwwlk  27167  clwwlknonex2  27256  upgr1wlkdlem1  27295  upgr3v3e3cycl  27330  upgr4cycl4dv4e  27335  eupth2lem3lem4  27381  frcond1  27418  frgr1v  27423  nfrgr2v  27424  frgr3v  27427  1vwmgr  27428  3vfriswmgrlem  27429  3vfriswmgr  27430  1to2vfriswmgr  27431  3cyclfrgrrn1  27437  4cycl2vnunb  27442  n4cyclfrgr  27443  vdgn1frgrv2  27448  frgrncvvdeqlem3  27453  frgrncvvdeqlem8  27458  frgrwopregbsn  27469  frgrwopreglem5ALT  27474  fusgr2wsp2nb  27486  esumpr2  30436  altopthsn  32372  dihprrn  37215  dvh3dim  37235  mapdindp2  37510  upgrwlkupwlk  42229  elsprel  42233  prelspr  42244  sprsymrelfolem2  42251
  Copyright terms: Public domain W3C validator