Theorem rcla4v 1864

Description: Restricted specialization with implicit substitution.

Hypothesis

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

Assertion

Ref	Expression
rcla4v	|- (A e. B -> (A.x e. B ph -> ps))

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

Proof of Theorem rcla4v

Step	Hyp	Ref	Expression
1		ax-17 968	. 2 |- (ps -> A.xps)
2		rcla4v.1	. 2 |- (x = A -> (ph <-> ps))
3	1, 2	rcla4 1862	1 |- (A e. B -> (A.x e. B ph -> ps))

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

This theorem is referenced by:  rcla4cv 1865  rcla4va 1866  rcla4dv 1869  rcla42v 1871  rcla43v 1873  intmin 2543  ralxfr 2889  wereu 2935  limuni3 3113  tfinds 3151  funcnvuni 3550  tfrlem2 3897  tz7.49 3944  oeordi 4198  nneneq 4492  unblem2 4518  unbnn2 4522  supub 4554  suplub 4555  rankun 4663  aceq3lem 4704  aceq5 4712  ac6lem 4726  numthlem 4755  unidom 4780  carduni 4830  alephval2 4874  cflim 4881  squeeze0 5872  nnleltp1t 5901  lbreu 5992  xrub 6027  dfuz 6150  uzwo5OLD 6159  uzwo3lem2 6165  zmax 6168  zbtwnre 6169  fzrevralt 6451  fsequb 6455  recant 6842  caubnd 6863  faclbnd4lem4 6888  bccl2t 6909  clm4le 7019  clmi1 7024  2climnn 7039  2climnn0 7040  climshft 7041  iserzshft2 7044  climaddlem3 7052  climmullem8 7063  climubi 7089  climcau 7092  caucvglem2 7094  caucvg 7099  serzf0 7105  ser1f0 7106  cvgratlem1ALT 7182  cvgratlem1 7185  cvgratlem4 7188  ivthlem6 7221  ivthlem7 7222  dsupivthlem 7226  ivthlem6OLD 7230  ivthlem7OLD 7231  unbenlem 7447  basgen2t 7581  clsval2 7627  metcnp 7826  lmle 7895  metelcls 7900  metcnp4 7904  metcn4i 7906  bcthlem2 7934  bcthlem16 7948  bcthlem17 7949  bcthlem33 7965  isgrp 7975  blocnilem 8395  ip2eqi 8448  minveclem27 8502  spwmo 8580  hial0 8889  hial02 8890  hial2eqt 8893  hlimunii 9029  ocorth 9080  occllem5 9093  projlem22 9123  projlem26 9127  h1de2 9391  pjjs 9562  lnopunilem1 9850  lnophmlem1 9856  nmcopexlem6 9871  nmcfnexlem6 9900  nlelch 9909  riesz4 9911  hmopidmch 9990  stge0t 10061  stle1t 10062  mdit 10132  mdbr3 10134  mdbr4 10135  dmdit 10139  dmdbr3 10141  dmdbr4 10142  dmdi4 10143  mdslmd1 10164  atss 10181  atom1d 10188  atmd 10234  sumdmdlem2 10253  cdj1 10265  cdj3 10273  ghomgrpilem1 10290  ghomf1olem 10301  cmphmp 10408  homcard 10426  cnfilca 10451

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