Theorem cla4ev 1865

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 1859	. 2 |- (A e. V -> (ps -> E.xph))
4	1, 3	ax-mp 7	1 |- (ps -> E.xph)

Syntax hints:   -> wi 3   <-> wb 146   = wceq 954   e. wcel 956  E.wex 978  Vcvv 1807

This theorem is referenced by:  el 2746  unipw 2751  nnullss 2763  exss 2764  dtru 2767  reusni 2888  opeldm 3309  xpnz 3458  ffoss 3702  ssimaex 3759  fvelrn 3803  dff2 3808  exfo 3813  elunirnALT 3860  fo1st 4081  fo2nd 4082  map0 4334  ensn1 4411  en1 4413  unen 4420  php3 4501  ssfi 4521  abfii3 4543  abfii4 4544  fodomfi 4546  inf0 4586  axinf2 4604  tz9.1 4626  r1pwcl 4667  rankuni 4678  scott0 4697  cplem2 4701  bnd2 4704  karden 4706  aceq3lem 4712  aceq4 4714  aceq5lem5 4719  aceq5 4720  aceq6a 4721  aceq6b 4722  ac6lem 4734  kmlem2 4746  kmlem13 4757  numthlem 4763  weth 4767  brdom3 4781  brdom7disj 4784  brdom6disj 4785  cfsuc 4895  axpowndlem3 4931  recmulpq 5050  dmrecpq 5054  ltexpq 5060  halfpq 5062  ltbtwnpq 5064  genpnmax 5090  1idpr 5113  ltexprlem7 5128  prlem936 5135  reclem1pr 5136  reclem2pr 5137  reclem3pr 5138  negexsr 5191  recexsrlem 5192  recexsr 5196  supsrlem5 5209  axrnegex 5263  axrrecex 5264  sup2 6006  nnunb 6025  climeu 7045  iserzext 7079  iserzex 7090  cvgcmp3ce 7131  isumsplit 7159  geoisum1c 7188  efseq1ex 7256  efseq0ex 7261  acdc3 7437  acdc2 7440  acdc5 7443  acdc 7445  infxpidmlem3 7505  subbas 7594  subbas2 7595  subtop 7596  lmfex 7910  metelcls 7916  pjrn 9587  cayleythlem 10347  infi 10484

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808

Copyright terms: Public domain