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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2209   A.wral 2528

This proof depends on 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 proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  raleqbidva  2767  poinxp  4844  funimass4  5753  fnmptfvd  5813  funimass3  5825  funconstss  5827  cocan1  5993  cocan2  5994  isocnv2  6018  isores2  6019  isoini2  6025  ofrfval  6311  ofrfval2  6319  dfsmo2  6558  smores  6563  smores2  6565  ac6sfi  7202  supisolem  7348  ordiso2  7375  ismkvnex  7495  nninfwlporlemd  7512  caucvgsrlemcau  8160  suplocsrlempr  8174  axsuploc  8398  suprleubex  9284  dfinfre  9286  zextlt  9738  prime  9745  infregelbex  9998  fzshftral  10515  nninfinf  10880  fimaxq  11270  swrdspsleq  11439  pfxeq  11468  clim  12047  clim2  12049  clim2c  12050  clim0c  12052  climabs0  12073  climrecvg1n  12114  mertenslem2  12303  mertensabs  12304  dfgcd2  12791  sqrt2irr  12940  pc11  13110  pcz  13111  1arith  13146  ballotfilemodife  13240  infpn2  13347  grpidpropdg  13694  sgrppropd  13728  mndpropd  13753  grppropd  13822  issubg4m  13996  rngpropd  14254  ringpropd  14343  oppr1g  14388  opprdrng  14620  lsspropdg  14768  isridlrng  14819  isridl  14841  expghmap  14942  assapropd  15014  psrbagconf1o  15064  tgss2  15180  neipsm  15255  ssidcn  15311  lmbrf  15316  cnnei  15333  cnrest2  15337  lmss  15347  lmres  15349  ismet2  15455  elmopn2  15550  metss  15595  metrest  15607  metcnp  15613  metcnp2  15614  metcn  15615  txmetcnp  15619  divcnap  15666  elcncf2  15675  mulc1cncf  15690  cncfmet  15693  cdivcncfap  15705  limcdifap  15763  limcmpted  15764  cnlimc  15773  mpodvdsmulf1o  16104  2sqlem6  16239  upgriswlkdc  16601  clwwlknonex2lem2  16679  iswomni0  17101  cndcap  17109