Theorem ralbidva 2529

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2202   A.wral 2511

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2516

This theorem is referenced by:  raleqbidva  2749  poinxp  4801  funimass4  5705  fnmptfvd  5760  funimass3  5772  funconstss  5774  cocan1  5938  cocan2  5939  isocnv2  5963  isores2  5964  isoini2  5970  ofrfval  6253  ofrfval2  6261  dfsmo2  6496  smores  6501  smores2  6503  ac6sfi  7130  supisolem  7267  ordiso2  7294  ismkvnex  7414  nninfwlporlemd  7431  caucvgsrlemcau  8073  suplocsrlempr  8087  axsuploc  8311  suprleubex  9193  dfinfre  9195  zextlt  9633  prime  9640  infregelbex  9893  fzshftral  10405  nninfinf  10768  fimaxq  11154  swrdspsleq  11314  pfxeq  11343  clim  11921  clim2  11923  clim2c  11924  clim0c  11926  climabs0  11947  climrecvg1n  11988  mertenslem2  12177  mertensabs  12178  dfgcd2  12665  sqrt2irr  12814  pc11  12984  pcz  12985  1arith  13020  infpn2  13157  grpidpropdg  13537  sgrppropd  13576  mndpropd  13603  grppropd  13680  issubg4m  13860  rngpropd  14049  ringpropd  14132  oppr1g  14176  lsspropdg  14527  isridlrng  14578  isridl  14600  expghmap  14703  psrbagconf1o  14774  tgss2  14890  neipsm  14965  ssidcn  15021  lmbrf  15026  cnnei  15043  cnrest2  15047  lmss  15057  lmres  15059  ismet2  15165  elmopn2  15260  metss  15305  metrest  15317  metcnp  15323  metcnp2  15324  metcn  15325  txmetcnp  15329  divcnap  15376  elcncf2  15385  mulc1cncf  15400  cncfmet  15403  cdivcncfap  15415  limcdifap  15473  limcmpted  15474  cnlimc  15483  mpodvdsmulf1o  15804  2sqlem6  15939  upgriswlkdc  16301  clwwlknonex2lem2  16379  iswomni0  16784  cndcap  16792