Theorem ralbidva 2486

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473

This theorem is referenced by:  raleqbidva  2700  poinxp  4713  funimass4  5586  fnmptfvd  5640  funimass3  5652  funconstss  5654  cocan1  5808  cocan2  5809  isocnv2  5833  isores2  5834  isoini2  5840  ofrfval  6114  ofrfval2  6122  dfsmo2  6311  smores  6316  smores2  6318  ac6sfi  6925  supisolem  7036  ordiso2  7063  ismkvnex  7182  nninfwlporlemd  7199  caucvgsrlemcau  7821  suplocsrlempr  7835  axsuploc  8059  suprleubex  8940  dfinfre  8942  zextlt  9374  prime  9381  infregelbex  9627  fzshftral  10137  fimaxq  10838  clim  11320  clim2  11322  clim2c  11323  clim0c  11325  climabs0  11346  climrecvg1n  11387  mertenslem2  11575  mertensabs  11576  dfgcd2  12046  sqrt2irr  12193  pc11  12362  pcz  12363  1arith  12398  infpn2  12506  grpidpropdg  12847  sgrppropd  12873  mndpropd  12898  grppropd  12959  issubg4m  13129  rngpropd  13306  ringpropd  13389  oppr1g  13429  lsspropdg  13744  isridlrng  13795  isridl  13816  tgss2  14031  neipsm  14106  ssidcn  14162  lmbrf  14167  cnnei  14184  cnrest2  14188  lmss  14198  lmres  14200  ismet2  14306  elmopn2  14401  metss  14446  metrest  14458  metcnp  14464  metcnp2  14465  metcn  14466  txmetcnp  14470  divcnap  14507  elcncf2  14513  mulc1cncf  14528  cncfmet  14531  cdivcncfap  14539  limcdifap  14583  limcmpted  14584  cnlimc  14593  2sqlem6  14920  iswomni0  15253  cndcap  15261