Theorem cla4ev 1860

Description: Existential specialization with implicit substitution. (The proof was shortened by Eric Schmidt, 22-Dec-2006.)

Hypotheses

Ref	Expression
cla4v.1	|- A e. V
cla4v.2	|- (x = A -> (ph <-> ps))

Assertion

Ref	Expression
cla4ev	|- (ps -> E.xph)

Distinct variable groups:   x,A   ps,x

Proof of Theorem cla4ev

Step	Hyp	Ref	Expression
1		cla4v.1	. 2 |- A e. V
2		cla4v.2	. . 3 |- (x = A -> (ph <-> ps))
3	2	cla4egv 1854	. 2 |- (A e. V -> (ps -> E.xph))
4	1, 3	ax-mp 7	1 |- (ps -> E.xph)

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

This theorem is referenced by:  el 2741  unipw 2746  nnullss 2758  exss 2759  dtru 2762  reusni 2883  opeldm 3303  xpnz 3452  ffoss 3696  ssimaex 3753  fvelrn 3797  dff2 3802  exfo 3807  elunirnALT 3854  fo1st 4075  fo2nd 4076  map0 4328  ensn1 4405  en1 4407  unen 4414  php3 4495  ssfi 4515  abfii3 4537  abfii4 4538  fodomfi 4540  inf0 4578  axinf2 4596  tz9.1 4618  r1pwcl 4659  rankuni 4670  scott0 4689  cplem2 4693  bnd2 4696  karden 4698  aceq3lem 4704  aceq4 4706  aceq5lem5 4711  aceq5 4712  aceq6a 4713  aceq6b 4714  ac6lem 4726  kmlem2 4738  kmlem13 4749  numthlem 4755  weth 4759  brdom3 4773  brdom7disj 4776  brdom6disj 4777  cfsuc 4887  axpowndlem3 4923  recmulpq 5042  dmrecpq 5046  ltexpq 5052  halfpq 5054  ltbtwnpq 5056  genpnmax 5082  1idpr 5105  ltexprlem7 5120  prlem936 5127  reclem1pr 5128  reclem2pr 5129  reclem3pr 5130  negexsr 5183  recexsrlem 5184  recexsr 5188  supsrlem5 5201  axrnegex 5255  axrrecex 5256  sup2 5998  nnunb 6017  climeu 7037  iserzext 7071  iserzex 7082  cvgcmp3ce 7123  isumsplit 7151  geoisum1c 7180  efseq1ex 7248  efseq0ex 7253  acdc3 7429  acdc2 7432  acdc5 7435  acdc 7437  infxpidmlem3 7497  subbas 7586  subbas2 7587  subtop 7588  lmfex 7894  metelcls 7900  pjrn 9564  cayleythlem 10320  infi 10448

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  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