Theorem ralbidva 2526

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  raleqbidva  2746  poinxp  4790  funimass4  5689  fnmptfvd  5744  funimass3  5756  funconstss  5758  cocan1  5920  cocan2  5921  isocnv2  5945  isores2  5946  isoini2  5952  ofrfval  6236  ofrfval2  6244  dfsmo2  6444  smores  6449  smores2  6451  ac6sfi  7073  supisolem  7191  ordiso2  7218  ismkvnex  7338  nninfwlporlemd  7355  caucvgsrlemcau  7996  suplocsrlempr  8010  axsuploc  8235  suprleubex  9117  dfinfre  9119  zextlt  9555  prime  9562  infregelbex  9810  fzshftral  10321  nninfinf  10682  fimaxq  11067  swrdspsleq  11220  pfxeq  11249  clim  11813  clim2  11815  clim2c  11816  clim0c  11818  climabs0  11839  climrecvg1n  11880  mertenslem2  12068  mertensabs  12069  dfgcd2  12556  sqrt2irr  12705  pc11  12875  pcz  12876  1arith  12911  infpn2  13048  grpidpropdg  13428  sgrppropd  13467  mndpropd  13494  grppropd  13571  issubg4m  13751  rngpropd  13939  ringpropd  14022  oppr1g  14066  lsspropdg  14416  isridlrng  14467  isridl  14489  expghmap  14592  tgss2  14774  neipsm  14849  ssidcn  14905  lmbrf  14910  cnnei  14927  cnrest2  14931  lmss  14941  lmres  14943  ismet2  15049  elmopn2  15144  metss  15189  metrest  15201  metcnp  15207  metcnp2  15208  metcn  15209  txmetcnp  15213  divcnap  15260  elcncf2  15269  mulc1cncf  15284  cncfmet  15287  cdivcncfap  15299  limcdifap  15357  limcmpted  15358  cnlimc  15367  mpodvdsmulf1o  15685  2sqlem6  15820  upgriswlkdc  16132  iswomni0  16533  cndcap  16541