Theorem ralbidva 2376

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 1466	. 2 |- F/ x ph
2		ralbidva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	1, 2	ralbida 2374	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

Syntax hints:   -> wi 4   /\ wa 102   <-> wb 103   e. wcel 1438   A.wral 2359

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464

This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364

This theorem is referenced by:  raleqbidva  2576  poinxp  4507  funimass4  5355  funimass3  5415  funconstss  5417  cocan1  5566  cocan2  5567  isocnv2  5591  isores2  5592  isoini2  5598  ofrfval  5864  ofrfval2  5871  dfsmo2  6052  smores  6057  smores2  6059  ac6sfi  6612  supisolem  6701  ordiso2  6726  caucvgsrlemcau  7336  suprleubex  8413  dfinfre  8415  zextlt  8836  prime  8843  fzshftral  9518  fimaxq  10231  clim  10665  clim2  10667  clim2c  10668  clim0c  10670  climabs0  10692  climrecvg1n  10733  mertenslem2  10926  mertensabs  10927  dfgcd2  11277  sqrt2irr  11415  elcncf2  11585  mulc1cncf  11600