Theorem ralbidva 2493

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  raleqbidva  2711  poinxp  4732  funimass4  5611  fnmptfvd  5666  funimass3  5678  funconstss  5680  cocan1  5834  cocan2  5835  isocnv2  5859  isores2  5860  isoini2  5866  ofrfval  6144  ofrfval2  6152  dfsmo2  6345  smores  6350  smores2  6352  ac6sfi  6959  supisolem  7074  ordiso2  7101  ismkvnex  7221  nninfwlporlemd  7238  caucvgsrlemcau  7860  suplocsrlempr  7874  axsuploc  8099  suprleubex  8981  dfinfre  8983  zextlt  9418  prime  9425  infregelbex  9672  fzshftral  10183  nninfinf  10535  fimaxq  10919  clim  11446  clim2  11448  clim2c  11449  clim0c  11451  climabs0  11472  climrecvg1n  11513  mertenslem2  11701  mertensabs  11702  dfgcd2  12181  sqrt2irr  12330  pc11  12500  pcz  12501  1arith  12536  infpn2  12673  grpidpropdg  13017  sgrppropd  13056  mndpropd  13081  grppropd  13149  issubg4m  13323  rngpropd  13511  ringpropd  13594  oppr1g  13638  lsspropdg  13987  isridlrng  14038  isridl  14060  expghmap  14163  tgss2  14315  neipsm  14390  ssidcn  14446  lmbrf  14451  cnnei  14468  cnrest2  14472  lmss  14482  lmres  14484  ismet2  14590  elmopn2  14685  metss  14730  metrest  14742  metcnp  14748  metcnp2  14749  metcn  14750  txmetcnp  14754  divcnap  14801  elcncf2  14810  mulc1cncf  14825  cncfmet  14828  cdivcncfap  14840  limcdifap  14898  limcmpted  14899  cnlimc  14908  mpodvdsmulf1o  15226  2sqlem6  15361  iswomni0  15695  cndcap  15703