Theorem rcla4cva 1867

Description: Restricted specialization with implicit substitution.

Hypothesis

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

Assertion

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

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

Proof of Theorem rcla4cva

Step	Hyp	Ref	Expression
1		rcla4v.1	. . 3 |- (x = A -> (ph <-> ps))
2	1	rcla4va 1866	. 2 |- ((A e. B /\ A.x e. B ph) -> ps)
3	2	ancoms 436	1 |- ((A.x e. B ph /\ A e. B) -> ps)

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

This theorem is referenced by:  disjne 2305  fconstfv 3834  odi 4194  omsmolem 4240  unblem1 4517  supmo 4550  sqr2irrlem3 6656  cau3ir 6852  climrecl 7047  climge0 7049  climcau 7092  infxpidmlem10 7504  elcls3 7652  iscncl 7709  metcnp 7826  cmscvg 7882  grpidinvlem3 7984  grpidinv 7986  grpidinv2 7994  vcid 8107  lnopeq0 9847  csmdsym 10169

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