Theorem rcla4cva 1872

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

This theorem is referenced by:  disjne 2311  fconstfv 3840  odi 4200  omsmolem 4246  unblem1 4523  supmo 4556  sqr2irrlem3 6664  cau3ir 6860  climrecl 7055  climge0 7057  climcau 7100  infxpidmlem10 7512  elcls3 7661  iscncl 7720  metcnp 7839  cmscvg 7898  grpidinvlem3 8000  grpidinv 8002  grpidinv2 8010  vcid 8122  lnopeq0 9870  csmdsym 10198

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