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  2686  poinxp  4695  funimass4  5566  fnmptfvd  5620  funimass3  5632  funconstss  5634  cocan1  5787  cocan2  5788  isocnv2  5812  isores2  5813  isoini2  5819  ofrfval  6090  ofrfval2  6098  dfsmo2  6287  smores  6292  smores2  6294  ac6sfi  6897  supisolem  7006  ordiso2  7033  ismkvnex  7152  nninfwlporlemd  7169  caucvgsrlemcau  7791  suplocsrlempr  7805  axsuploc  8029  suprleubex  8910  dfinfre  8912  zextlt  9344  prime  9351  infregelbex  9597  fzshftral  10107  fimaxq  10806  clim  11288  clim2  11290  clim2c  11291  clim0c  11293  climabs0  11314  climrecvg1n  11355  mertenslem2  11543  mertensabs  11544  dfgcd2  12014  sqrt2irr  12161  pc11  12329  pcz  12330  1arith  12364  infpn2  12456  grpidpropdg  12792  mndpropd  12840  grppropd  12892  issubg4m  13051  ringpropd  13215  oppr1g  13250  tgss2  13549  neipsm  13624  ssidcn  13680  lmbrf  13685  cnnei  13702  cnrest2  13706  lmss  13716  lmres  13718  ismet2  13824  elmopn2  13919  metss  13964  metrest  13976  metcnp  13982  metcnp2  13983  metcn  13984  txmetcnp  13988  divcnap  14025  elcncf2  14031  mulc1cncf  14046  cncfmet  14049  cdivcncfap  14057  limcdifap  14101  limcmpted  14102  cnlimc  14111  2sqlem6  14437  iswomni0  14769