Theorem ceqsexv 1371

Description: Elimination of an existential quantifier, using implicit substitution.

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 group(s):   x,A   ps,x

Proof of Theorem ceqsexv

Step	Hyp	Ref	Expression
1		ax-17 925	. 2 |- (ps -> A.xps)
2		ceqsexv.1	. 2 |- A e. V
3		ceqsexv.2	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	ceqsex 1370	1 |- (E.x(x = A /\ ph) <-> ps)

Syntax hints:   -> wi 2   <-> wb 127   /\ wa 196  E.wex 678   = wceq 1091   e. wcel 1092  Vcvv 1348

This theorem is referenced by:  gencbvex 1372  clel3 1375  euxfr2 1435  vsbcint 1438  zfaus 1480  eqvinop 1901  iunxsn 2034  cbvop 2473  iss 2599  imai 2613  elimasn 2617  intirr 2628  elxp4 2640  elxp5 2641  coi1 2665  fcoi1 2765  fcoi2 2766  fv2 2828  dmfco 2864  fvco 2865  ec2 3203  snec 3232  mapsnen 3334  xpsnen 3339  xpassen 3344  aceq5lem1 3558  aceq5lem2 3559  aceq5lem3 3560  cf0 3705  distrlem1pr 3921  ltexprlem4 3939  infxpidmlem8 4940

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org