Theorem ceqsexv 1826

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 968	. 2 |- (ps -> A.xps)
2		ceqsexv.1	. 2 |- A e. V
3		ceqsexv.2	. 2 |- (x = A -> (ph <-> ps))
4	1, 2, 3	ceqsex 1825	1 |- (E.x(x = A /\ ph) <-> ps)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977  Vcvv 1802

This theorem is referenced by:  gencbvex 1829  euxfr2 1916  sbhypf 1929  sbhyp 1930  iunxsn 2602  eqvinop 2781  dfid3 2826  uniuni 2870  iss 3381  imai 3401  elimasn 3410  intirr 3427  elxp4 3439  elxp5 3440  coi1 3496  fcoi1 3630  fcoi2 3631  fv2 3705  dmfco 3758  fvco 3759  2ndconst 4081  oarec 4180  dfec2 4248  snec 4280  mapsnen 4410  xpsnen 4415  xpassen 4421  aceq5lem1 4707  aceq5lem2 4708  aceq5lem3 4709  cf0 4882  distrlem1pr 5099  ltexprlem4 5117  ssxr 5513  infxpidmlem8 7502  subtop 7588  nmcopexlem1 9866  nmcfnexlem1 9895  ntunte 10340

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803

Copyright terms: Public domain