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

Theorem ceqsexv 2991
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 1629 . 2  |-  F/ x ps
2 ceqsexv.1 . 2  |-  A  e. 
_V
3 ceqsexv.2 . 2  |-  ( x  =  A  ->  ( ph 
<->  ps ) )
41, 2, 3ceqsex 2990 1  |-  ( E. x ( x  =  A  /\  ph )  <->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   E.wex 1550    = wceq 1652    e. wcel 1725   _Vcvv 2956
This theorem is referenced by:  ceqsex3v  2994  gencbvex  2998  sbhypf  3001  euxfr2  3119  inuni  4362  eqvinop  4441  dfid3  4499  uniuni  4716  opeliunxp  4929  elvvv  4937  imai  5218  elxp4  5357  elxp5  5358  coi1  5385  dmfco  5797  fndmdif  5834  fndmin  5837  fmptco  5901  abrexco  5986  opabex3d  5989  opabex3  5990  fsplit  6451  brtpos2  6485  mapsnen  7184  xpsnen  7192  xpcomco  7198  xpassen  7202  dfac5lem1  8004  dfac5lem2  8005  dfac5lem3  8006  cf0  8131  ltexprlem4  8916  pceu  13220  4sqlem12  13324  vdwapun  13342  gsumval3eu  15513  dprd2d2  15602  znleval  16835  metrest  18554  ceqsexv2d  23985  fmptcof2  24076  dfdm5  25400  dfrn5  25401  elima4  25404  nofulllem5  25661  brtxp  25725  brpprod  25730  elfix  25748  dffix2  25750  sscoid  25758  elfuns  25760  dfiota3  25768  brimg  25782  brapply  25783  brsuccf  25786  funpartlem  25787  brrestrict  25794  dfrdg4  25795  tfrqfree  25796  diophrex  26834  lshpsmreu  29907  isopos  29978  islpln5  30332  islvol5  30376  pmapglb  30567  polval2N  30703  cdlemftr3  31362  dibelval3  31945  dicelval3  31978  mapdpglem3  32473  hdmapglem7a  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-v 2958
  Copyright terms: Public domain W3C validator