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  6563  smores  6568  smores2  6570  ac6sfi  7208  supisolem  7354  ordiso2  7381  ismkvnex  7501  nninfwlporlemd  7518  caucvgsrlemcau  8166  suplocsrlempr  8180  axsuploc  8404  suprleubex  9292  dfinfre  9294  ofsubeq0  9300  zextlt  9748  prime  9755  infregelbex  10013  fzshftral  10531  nninfinf  10900  fimaxq  11291  swrdspsleq  11460  pfxeq  11489  clim  12071  clim2  12073  clim2c  12074  clim0c  12076  climabs0  12097  climrecvg1n  12138  mertenslem2  12327  mertensabs  12328  dfgcd2  12815  sqrt2irr  12965  pc11  13138  pcz  13139  1arith  13174  ballotfilemodife  13297  infpn2  13404  grpidpropdg  13752  sgrppropd  13786  mndpropd  13811  grppropd  13880  issubg4m  14054  rngpropd  14360  ringpropd  14449  oppr1g  14496  opprdrng  14728  lsspropdg  14876  isridlrng  14927  isridl  14949  expghmap  15050  assapropd  15122  psrbagconf1o  15177  gsumbagdiaglem  15184  tgss2  15322  neipsm  15397  ssidcn  15453  lmbrf  15458  cnnei  15475  cnrest2  15479  lmss  15489  lmres  15491  ismet2  15597  elmopn2  15692  metss  15737  metrest  15749  metcnp  15755  metcnp2  15756  metcn  15757  txmetcnp  15761  divcnap  15808  elcncf2  15817  mulc1cncf  15832  cncfmet  15835  cdivcncfap  15847  limcdifap  15905  limcmpted  15906  cnlimc  15915  mpodvdsmulf1o  16301  2sqlem6  16461  upgriswlkdc  16823  clwwlknonex2lem2  16901  iswomni0  17325  cndcap  17333