Theorem ralbidva 2473

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2148   A.wral 2455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  raleqbidva  2687  poinxp  4697  funimass4  5568  fnmptfvd  5622  funimass3  5634  funconstss  5636  cocan1  5790  cocan2  5791  isocnv2  5815  isores2  5816  isoini2  5822  ofrfval  6093  ofrfval2  6101  dfsmo2  6290  smores  6295  smores2  6297  ac6sfi  6900  supisolem  7009  ordiso2  7036  ismkvnex  7155  nninfwlporlemd  7172  caucvgsrlemcau  7794  suplocsrlempr  7808  axsuploc  8032  suprleubex  8913  dfinfre  8915  zextlt  9347  prime  9354  infregelbex  9600  fzshftral  10110  fimaxq  10809  clim  11291  clim2  11293  clim2c  11294  clim0c  11296  climabs0  11317  climrecvg1n  11358  mertenslem2  11546  mertensabs  11547  dfgcd2  12017  sqrt2irr  12164  pc11  12332  pcz  12333  1arith  12367  infpn2  12459  grpidpropdg  12798  mndpropd  12846  grppropd  12898  issubg4m  13058  ringpropd  13222  oppr1g  13257  tgss2  13618  neipsm  13693  ssidcn  13749  lmbrf  13754  cnnei  13771  cnrest2  13775  lmss  13785  lmres  13787  ismet2  13893  elmopn2  13988  metss  14033  metrest  14045  metcnp  14051  metcnp2  14052  metcn  14053  txmetcnp  14057  divcnap  14094  elcncf2  14100  mulc1cncf  14115  cncfmet  14118  cdivcncfap  14126  limcdifap  14170  limcmpted  14171  cnlimc  14180  2sqlem6  14506  iswomni0  14838  cndcap  14846