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

Theorem ceqsexv 2823
Description: Elimination of an existential quantifier, using implicit substitution. (Contributed by NM, 2-Mar-1995.)
Hypotheses
Ref Expression
ceqsexv.1  |-  A  e. 
_V
ceqsexv.2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
ceqsexv  |-  ( E. x ( x  =  A  /\  ph )  <->  ps )
Distinct variable groups:    x, A    ps, x
Allowed substitution hint:    ph( x)

Proof of Theorem ceqsexv
StepHypRef Expression
1 nfv 1605 . 2  |-  F/ x ps
2 ceqsexv.1 . 2  |-  A  e. 
_V
3 ceqsexv.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3ceqsex 2822 1  |-  ( E. x ( x  =  A  /\  ph )  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358   E.wex 1528    = wceq 1623    e. wcel 1684   _Vcvv 2788
This theorem is referenced by:  ceqsex3v  2826  gencbvex  2830  sbhypf  2833  euxfr2  2950  inuni  4173  eqvinop  4251  dfid3  4310  uniuni  4527  opeliunxp  4740  elvvv  4749  imai  5027  elxp4  5160  elxp5  5161  coi1  5188  dmfco  5593  fndmdif  5629  fndmin  5632  fmptco  5691  abrexco  5766  opabex3  5769  fsplit  6223  brtpos2  6240  mapsnen  6938  xpsnen  6946  xpcomco  6952  xpassen  6956  dfac5lem1  7750  dfac5lem2  7751  dfac5lem3  7752  cf0  7877  ltexprlem4  8663  pceu  12899  4sqlem12  13003  vdwapun  13021  gsumval3eu  15190  dprd2d2  15279  znleval  16508  metrest  18070  ceqsexv2d  23162  fmptcof2  23229  dfdm5  24132  dfrn5  24133  nofulllem5  24360  brtxp  24420  brpprod  24425  dffun10  24453  dfiota3  24462  brimg  24476  brapply  24477  brcup  24478  brcap  24479  brsuccf  24480  funpartfun  24481  funpartfv  24483  brrestrict  24487  dfrdg4  24488  tfrqfree  24489  eqvinopb  24965  diophrex  26855  lshpsmreu  29299  isopos  29370  islpln5  29724  islvol5  29768  pmapglb  29959  polval2N  30095  cdlemftr3  30754  dibelval3  31337  dicelval3  31370  mapdpglem3  31865  hdmapglem7a  32120
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-v 2790
  Copyright terms: Public domain W3C validator