Theorem ralbidva 2364

Description: Formula-building rule for restricted universal quantifier (deduction rule). (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 1461	. 2 |- F/ x ph
2		ralbidva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	1, 2	ralbida 2362	1 |- ( ph -> ( A. x e. A ps <-> A. x e. A ch ) )

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

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 1376  ax-gen 1378  ax-4 1440  ax-17 1459

This theorem depends on definitions:  df-bi 115  df-nf 1390  df-ral 2353

This theorem is referenced by:  raleqbidva  2563  poinxp  4427  funimass4  5245  funimass3  5304  funconstss  5306  cocan1  5447  cocan2  5448  isocnv2  5472  isores2  5473  isoini2  5478  ofrfval  5740  ofrfval2  5747  dfsmo2  5925  smores  5930  smores2  5932  ac6sfi  6379  supisolem  6421  ordiso2  6446  caucvgsrlemcau  6969  suprleubex  8032  dfinfre  8034  zextlt  8439  prime  8446  fzshftral  9125  clim  10120  clim2  10122  clim2c  10123  clim0c  10125  climabs0  10146  climrecvg1n  10185  dfgcd2  10403  sqrt2irr  10541