Theorem ralbidva 2387

Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.)

Hypothesis

Ref	Expression
ralbidva.1	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )

Assertion

Ref	Expression
ralbidva	|- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem ralbidva

Step	Hyp	Ref	Expression
1		nfv 1473	. 2 |- F/ x ph
2		ralbidva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	1, 2	ralbida 2385	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   e. wcel 1445   A.wral 2370

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375

This theorem is referenced by:  raleqbidva  2590  poinxp  4536  funimass4  5390  funimass3  5454  funconstss  5456  cocan1  5604  cocan2  5605  isocnv2  5629  isores2  5630  isoini2  5636  ofrfval  5902  ofrfval2  5909  dfsmo2  6090  smores  6095  smores2  6097  ac6sfi  6694  supisolem  6783  ordiso2  6808  caucvgsrlemcau  7435  suprleubex  8512  dfinfre  8514  zextlt  8937  prime  8944  fzshftral  9671  fimaxq  10350  clim  10824  clim2  10826  clim2c  10827  clim0c  10829  climabs0  10850  climrecvg1n  10891  mertenslem2  11079  mertensabs  11080  dfgcd2  11430  sqrt2irr  11568  tgss2  11931  neipsm  12006  ssidcn  12061  lmbrf  12066  cnnei  12083  cnrest2  12087  lmss  12097  lmres  12099  ismet2  12140  elmopn2  12235  metss  12280  metrest  12292  metcnp  12294  metcnp2  12295  metcn  12296  elcncf2  12327  mulc1cncf  12342  cncfmet  12345  cdivcncfap  12350