Theorem ralbidva 2462

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

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

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  raleqbidva  2675  poinxp  4673  funimass4  5537  funimass3  5601  funconstss  5603  cocan1  5755  cocan2  5756  isocnv2  5780  isores2  5781  isoini2  5787  ofrfval  6058  ofrfval2  6066  dfsmo2  6255  smores  6260  smores2  6262  ac6sfi  6864  supisolem  6973  ordiso2  7000  ismkvnex  7119  caucvgsrlemcau  7734  suplocsrlempr  7748  axsuploc  7971  suprleubex  8849  dfinfre  8851  zextlt  9283  prime  9290  infregelbex  9536  fzshftral  10043  fimaxq  10740  clim  11222  clim2  11224  clim2c  11225  clim0c  11227  climabs0  11248  climrecvg1n  11289  mertenslem2  11477  mertensabs  11478  dfgcd2  11947  sqrt2irr  12094  pc11  12262  pcz  12263  1arith  12297  infpn2  12389  grpidpropdg  12605  tgss2  12719  neipsm  12794  ssidcn  12850  lmbrf  12855  cnnei  12872  cnrest2  12876  lmss  12886  lmres  12888  ismet2  12994  elmopn2  13089  metss  13134  metrest  13146  metcnp  13152  metcnp2  13153  metcn  13154  txmetcnp  13158  divcnap  13195  elcncf2  13201  mulc1cncf  13216  cncfmet  13219  cdivcncfap  13227  limcdifap  13271  limcmpted  13272  cnlimc  13281  2sqlem6  13596  iswomni0  13930