Theorem rcla4va 1866

Description: Restricted specialization with implicit substitution.

Hypothesis

Ref	Expression
rcla4v.1	|- (x = A -> (ph <-> ps))

Assertion

Ref	Expression
rcla4va	|- ((A e. B /\ A.x e. B ph) -> ps)

Distinct variable groups:   x,A   x,B   ps,x

Proof of Theorem rcla4va

Step	Hyp	Ref	Expression
1		rcla4v.1	. . 3 |- (x = A -> (ph <-> ps))
2	1	rcla4v 1864	. 2 |- (A e. B -> (A.x e. B ph -> ps))
3	2	imp 350	1 |- ((A e. B /\ A.x e. B ph) -> ps)

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 953   e. wcel 955  A.wral 1637

This theorem is referenced by:  rcla4cva 1867  unifi 4532  supmo 4550  noinfep 4612  nnleltp1t 5901  infmrcl 6016  xrsupsslem 6023  xrinfmsslem 6024  supxrunb1 6036  supxrunb2 6037  zextlet 6136  fsequb 6455  seqzfveq 6486  faclbnd4lem4 6888  climaddlem1 7050  climmullem6 7061  serzf0 7105  ser1f0 7106  isum1p 7141  iserzgt0 7146  opnin 7809  lpbl 7819  bcthlem18 7950  grpidinvlem3 7984  grpideu 7987  lnopcon 9878  lnfncon 9905  nlelch 9909  homcard 10426

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-ral 1641  df-v 1803

Copyright terms: Public domain