Theorem ralbidva 2504

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

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  raleqbidva  2723  poinxp  4762  funimass4  5652  fnmptfvd  5707  funimass3  5719  funconstss  5721  cocan1  5879  cocan2  5880  isocnv2  5904  isores2  5905  isoini2  5911  ofrfval  6190  ofrfval2  6198  dfsmo2  6396  smores  6401  smores2  6403  ac6sfi  7021  supisolem  7136  ordiso2  7163  ismkvnex  7283  nninfwlporlemd  7300  caucvgsrlemcau  7941  suplocsrlempr  7955  axsuploc  8180  suprleubex  9062  dfinfre  9064  zextlt  9500  prime  9507  infregelbex  9754  fzshftral  10265  nninfinf  10625  fimaxq  11009  swrdspsleq  11158  pfxeq  11187  clim  11707  clim2  11709  clim2c  11710  clim0c  11712  climabs0  11733  climrecvg1n  11774  mertenslem2  11962  mertensabs  11963  dfgcd2  12450  sqrt2irr  12599  pc11  12769  pcz  12770  1arith  12805  infpn2  12942  grpidpropdg  13321  sgrppropd  13360  mndpropd  13387  grppropd  13464  issubg4m  13644  rngpropd  13832  ringpropd  13915  oppr1g  13959  lsspropdg  14308  isridlrng  14359  isridl  14381  expghmap  14484  tgss2  14666  neipsm  14741  ssidcn  14797  lmbrf  14802  cnnei  14819  cnrest2  14823  lmss  14833  lmres  14835  ismet2  14941  elmopn2  15036  metss  15081  metrest  15093  metcnp  15099  metcnp2  15100  metcn  15101  txmetcnp  15105  divcnap  15152  elcncf2  15161  mulc1cncf  15176  cncfmet  15179  cdivcncfap  15191  limcdifap  15249  limcmpted  15250  cnlimc  15259  mpodvdsmulf1o  15577  2sqlem6  15712  iswomni0  16192  cndcap  16200