Theorem rcla4cv 1865

Description: Restricted specialization with implicit substitution.

Hypothesis

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

Assertion

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

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

Proof of Theorem rcla4cv

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	com12 11	1 |- (A.x e. B ph -> (A e. B -> ps))

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

This theorem is referenced by:  limsuc 3110  limuni3 3113  ralxp 3208  dff2 3802  abianfp 3947  odi 4194  elirrv 4570  dfom3 4602  aceq5lem5 4711  aceq6b 4714  zorn2lem2 4761  zorn2lem6 4765  unidom 4780  alephle 4856  peano2nn 5883  sqr2irrlem3 6656  seq1ublem 6848  cvg2 6859  serzcl2t 6987  caucvg 7099  basis2t 7557  tg2t 7563  tgval3t 7567  basgen2t 7581  clsndisj 7648  cnpimaex 7704  cnima 7706  cnclima 7710  opni 7804  metcnpi 7829  metcnpi2 7830  lmcvg 7870  caun0 7880  metcnp4lem2 7903  iscms2lem5 7927  lmcau 7930  nvz 8236  nmoubi 8367  pslem 8573  chcompl 9036  ocin 9085  occllem6 9094  pjthlem12 9145  nmopubt 9749  cnopct 9753  nmfnleubt 9765  cnfnct 9770  dmdmdt 10137  mdsl1 10156  idosd 10521

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