Theorem ceqsexv 1835

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 groups:   x,A   ps,x

Proof of Theorem ceqsexv

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

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980  Vcvv 1811

This theorem is referenced by:  gencbvex 1838  euxfr2 1926  sbhypf 1939  sbhyp 1940  iunxsn 2612  eqvinop 2791  dfid3 2836  uniuni 2880  iss 3397  imai 3417  elimasn 3426  intirr 3441  elxp4 3453  elxp5 3454  coi1 3510  fcoi1 3645  fcoi2 3646  fv2 3720  dmfco 3773  fvco 3774  2ndconst 4097  oarec 4196  dfec2 4264  snec 4296  mapsnen 4429  xpsnen 4435  xpassen 4441  aceq5lem1 4735  aceq5lem2 4736  aceq5lem3 4737  cf0 4910  distrlem1pr 5127  ltexprlem4 5145  ssxr 5540  infxpidmlem8 7559  subtop 7646  nmcopexlem1 9951  nmcfnexlem1 9980  ntunte 10439

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain