Theorem ralbidva 2546

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

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

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is referenced by:  raleqbidva  2767  poinxp  4839  funimass4  5747  fnmptfvd  5804  funimass3  5816  funconstss  5818  cocan1  5983  cocan2  5984  isocnv2  6008  isores2  6009  isoini2  6015  ofrfval  6301  ofrfval2  6309  dfsmo2  6548  smores  6553  smores2  6555  ac6sfi  7192  supisolem  7338  ordiso2  7365  ismkvnex  7485  nninfwlporlemd  7502  caucvgsrlemcau  8150  suplocsrlempr  8164  axsuploc  8388  suprleubex  9274  dfinfre  9276  zextlt  9717  prime  9724  infregelbex  9977  fzshftral  10493  nninfinf  10858  fimaxq  11248  swrdspsleq  11417  pfxeq  11446  clim  12025  clim2  12027  clim2c  12028  clim0c  12030  climabs0  12051  climrecvg1n  12092  mertenslem2  12281  mertensabs  12282  dfgcd2  12769  sqrt2irr  12918  pc11  13088  pcz  13089  1arith  13124  ballotfilemodife  13218  infpn2  13325  grpidpropdg  13671  sgrppropd  13705  mndpropd  13730  grppropd  13799  issubg4m  13973  rngpropd  14229  ringpropd  14316  oppr1g  14361  opprdrng  14593  lsspropdg  14740  isridlrng  14791  isridl  14813  expghmap  14914  psrbagconf1o  14987  tgss2  15103  neipsm  15178  ssidcn  15234  lmbrf  15239  cnnei  15256  cnrest2  15260  lmss  15270  lmres  15272  ismet2  15378  elmopn2  15473  metss  15518  metrest  15530  metcnp  15536  metcnp2  15537  metcn  15538  txmetcnp  15542  divcnap  15589  elcncf2  15598  mulc1cncf  15613  cncfmet  15616  cdivcncfap  15628  limcdifap  15686  limcmpted  15687  cnlimc  15696  mpodvdsmulf1o  16018  2sqlem6  16153  upgriswlkdc  16515  clwwlknonex2lem2  16593  iswomni0  17006  cndcap  17014