Theorem rcla4cv 1870

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 1869	. 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 954   e. wcel 956  A.wral 1642

This theorem is referenced by:  limsuc 3115  limuni3 3118  ralxp 3213  dff2 3808  abianfp 3953  odi 4200  elirrv 4578  dfom3 4610  aceq5lem5 4719  aceq6b 4722  zorn2lem2 4769  zorn2lem6 4773  unidom 4788  alephle 4864  peano2nn 5891  sqr2irrlem3 6664  seq1ublem 6856  cvg2 6867  serzcl2t 6995  caucvg 7107  basis2t 7565  tg2t 7571  tgval3t 7575  basgen2t 7589  clsndisj 7656  cnpimaex 7715  cnima 7717  cnclima 7721  opni 7816  metcnpi 7842  metcnpi2 7843  lmcvg 7884  caun0 7896  metcnp4lem2 7919  iscms2lem5 7943  lmcau 7946  nvz 8249  nmoubi 8380  pslem 8590  chcompl 9054  ocin 9108  occllem6 9117  pjthlem12 9168  nmopubt 9772  cnopct 9776  nmfnleubt 9788  cnfnct 9793  dmdmdt 10165  mdsl1 10185  idosd 10557

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-ral 1646  df-v 1808

Copyright terms: Public domain