Theorem ralbidva 2460

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-4 1497  ax-17 1513

This theorem depends on definitions:  df-bi 116  df-nf 1448  df-ral 2447

This theorem is referenced by:  raleqbidva  2673  poinxp  4667  funimass4  5531  funimass3  5595  funconstss  5597  cocan1  5749  cocan2  5750  isocnv2  5774  isores2  5775  isoini2  5781  ofrfval  6052  ofrfval2  6060  dfsmo2  6246  smores  6251  smores2  6253  ac6sfi  6855  supisolem  6964  ordiso2  6991  ismkvnex  7110  caucvgsrlemcau  7725  suplocsrlempr  7739  axsuploc  7962  suprleubex  8840  dfinfre  8842  zextlt  9274  prime  9281  infregelbex  9527  fzshftral  10033  fimaxq  10729  clim  11208  clim2  11210  clim2c  11211  clim0c  11213  climabs0  11234  climrecvg1n  11275  mertenslem2  11463  mertensabs  11464  dfgcd2  11932  sqrt2irr  12071  pc11  12239  pcz  12240  tgss2  12620  neipsm  12695  ssidcn  12751  lmbrf  12756  cnnei  12773  cnrest2  12777  lmss  12787  lmres  12789  ismet2  12895  elmopn2  12990  metss  13035  metrest  13047  metcnp  13053  metcnp2  13054  metcn  13055  txmetcnp  13059  divcnap  13096  elcncf2  13102  mulc1cncf  13117  cncfmet  13120  cdivcncfap  13128  limcdifap  13172  limcmpted  13173  cnlimc  13182  iswomni0  13764