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  4846  funimass4  5756  fnmptfvd  5816  funimass3  5828  funconstss  5830  cocan1  5996  cocan2  5997  isocnv2  6021  isores2  6022  isoini2  6028  ofrfval  6315  ofrfval2  6323  dfsmo2  6562  smores  6567  smores2  6569  ac6sfi  7206  supisolem  7354  ordiso2  7381  ismkvnex  7501  nninfwlporlemd  7518  caucvgsrlemcau  8166  suplocsrlempr  8180  axsuploc  8404  suprleubex  9292  dfinfre  9294  ofsubeq0  9300  zextlt  9749  prime  9756  infregelbex  10014  fzshftral  10532  nninfinf  10901  fimaxq  11292  swrdspsleq  11461  pfxeq  11490  clim  12072  clim2  12074  clim2c  12075  clim0c  12077  climabs0  12098  climrecvg1n  12139  mertenslem2  12328  mertensabs  12329  dfgcd2  12816  sqrt2irr  12966  pc11  13139  pcz  13140  1arith  13175  ballotfilemodife  13298  infpn2  13405  grpidpropdg  13753  sgrppropd  13787  mndpropd  13812  grppropd  13881  issubg4m  14055  rngpropd  14361  ringpropd  14450  oppr1g  14497  opprdrng  14729  lsspropdg  14877  isridlrng  14928  isridl  14950  expghmap  15051  assapropd  15123  psrbagconf1o  15174  gsumbagdiaglem  15175  tgss2  15305  neipsm  15380  ssidcn  15436  lmbrf  15441  cnnei  15458  cnrest2  15462  lmss  15472  lmres  15474  ismet2  15580  elmopn2  15675  metss  15720  metrest  15732  metcnp  15738  metcnp2  15739  metcn  15740  txmetcnp  15744  divcnap  15791  elcncf2  15800  mulc1cncf  15815  cncfmet  15818  cdivcncfap  15830  limcdifap  15888  limcmpted  15889  cnlimc  15898  mpodvdsmulf1o  16284  2sqlem6  16444  upgriswlkdc  16806  clwwlknonex2lem2  16884  iswomni0  17308  cndcap  17316