Theorem ralbidva 2466

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

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

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  raleqbidva  2679  poinxp  4680  funimass4  5547  fnmptfvd  5600  funimass3  5612  funconstss  5614  cocan1  5766  cocan2  5767  isocnv2  5791  isores2  5792  isoini2  5798  ofrfval  6069  ofrfval2  6077  dfsmo2  6266  smores  6271  smores2  6273  ac6sfi  6876  supisolem  6985  ordiso2  7012  ismkvnex  7131  nninfwlporlemd  7148  caucvgsrlemcau  7755  suplocsrlempr  7769  axsuploc  7992  suprleubex  8870  dfinfre  8872  zextlt  9304  prime  9311  infregelbex  9557  fzshftral  10064  fimaxq  10762  clim  11244  clim2  11246  clim2c  11247  clim0c  11249  climabs0  11270  climrecvg1n  11311  mertenslem2  11499  mertensabs  11500  dfgcd2  11969  sqrt2irr  12116  pc11  12284  pcz  12285  1arith  12319  infpn2  12411  grpidpropdg  12628  mndpropd  12676  grppropd  12724  tgss2  12873  neipsm  12948  ssidcn  13004  lmbrf  13009  cnnei  13026  cnrest2  13030  lmss  13040  lmres  13042  ismet2  13148  elmopn2  13243  metss  13288  metrest  13300  metcnp  13306  metcnp2  13307  metcn  13308  txmetcnp  13312  divcnap  13349  elcncf2  13355  mulc1cncf  13370  cncfmet  13373  cdivcncfap  13381  limcdifap  13425  limcmpted  13426  cnlimc  13435  2sqlem6  13750  iswomni0  14083