Theorem ralbidva 2431

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

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

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419

This theorem is referenced by:  raleqbidva  2638  poinxp  4603  funimass4  5465  funimass3  5529  funconstss  5531  cocan1  5681  cocan2  5682  isocnv2  5706  isores2  5707  isoini2  5713  ofrfval  5983  ofrfval2  5991  dfsmo2  6177  smores  6182  smores2  6184  ac6sfi  6785  supisolem  6888  ordiso2  6913  ismkvnex  7022  caucvgsrlemcau  7594  suplocsrlempr  7608  axsuploc  7830  suprleubex  8705  dfinfre  8707  zextlt  9136  prime  9143  fzshftral  9881  fimaxq  10566  clim  11043  clim2  11045  clim2c  11046  clim0c  11048  climabs0  11069  climrecvg1n  11110  mertenslem2  11298  mertensabs  11299  dfgcd2  11691  sqrt2irr  11829  tgss2  12237  neipsm  12312  ssidcn  12368  lmbrf  12373  cnnei  12390  cnrest2  12394  lmss  12404  lmres  12406  ismet2  12512  elmopn2  12607  metss  12652  metrest  12664  metcnp  12670  metcnp2  12671  metcn  12672  txmetcnp  12676  divcnap  12713  elcncf2  12719  mulc1cncf  12734  cncfmet  12737  cdivcncfap  12745  limcdifap  12789  limcmpted  12790  cnlimc  12799