MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ceqsexv Unicode version

Theorem ceqsexv 3146
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)
Hypotheses
Ref Expression
ceqsexv.1
ceqsexv.2
Assertion
Ref Expression
ceqsexv
Distinct variable groups:   ,   ,

Proof of Theorem ceqsexv
StepHypRef Expression
1 nfv 1707 . 2
2 ceqsexv.1 . 2
3 ceqsexv.2 . 2
41, 2, 3ceqsex 3145 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818   cvv 3109
This theorem is referenced by:  ceqsex3v  3149  gencbvex  3153  sbhypf  3156  euxfr2  3284  inuni  4614  eqvinop  4736  dfid3  4801  opeliunxp  5056  elvvv  5064  imai  5354  coi1  5528  dmfco  5947  fndmdif  5991  fndmin  5994  fmptco  6064  abrexco  6156  uniuni  6609  elxp4  6744  elxp5  6745  opabex3d  6778  opabex3  6779  fsplit  6905  brtpos2  6980  mapsnen  7613  xpsnen  7621  xpcomco  7627  xpassen  7631  dfac5lem1  8525  dfac5lem2  8526  dfac5lem3  8527  cf0  8652  ltexprlem4  9438  pceu  14370  4sqlem12  14474  vdwapun  14492  gsumval3eu  16907  dprd2d2  17093  znleval  18593  metrest  21027  ceqsexv2d  27397  fmptcof2  27502  fpwrelmapffslem  27555  dfdm5  29206  dfrn5  29207  elima4  29209  nofulllem5  29466  brtxp  29530  brpprod  29535  elfix  29553  dffix2  29555  sscoid  29563  elfuns  29565  dfiota3  29573  brimg  29587  brapply  29588  brsuccf  29591  funpartlem  29592  brrestrict  29599  dfrdg4  29600  tfrqfree  29601  diophrex  30709  opeliun2xp  32922  lshpsmreu  34834  isopos  34905  islpln5  35259  islvol5  35303  pmapglb  35494  polval2N  35630  cdlemftr3  36291  dibelval3  36874  dicelval3  36907  mapdpglem3  37402  hdmapglem7a  37657
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-12 1854  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111
  Copyright terms: Public domain W3C validator