Theorem ralbidva 2490

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

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

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2477

This theorem is referenced by:  raleqbidva  2708  poinxp  4729  funimass4  5608  fnmptfvd  5663  funimass3  5675  funconstss  5677  cocan1  5831  cocan2  5832  isocnv2  5856  isores2  5857  isoini2  5863  ofrfval  6141  ofrfval2  6149  dfsmo2  6342  smores  6347  smores2  6349  ac6sfi  6956  supisolem  7069  ordiso2  7096  ismkvnex  7216  nninfwlporlemd  7233  caucvgsrlemcau  7855  suplocsrlempr  7869  axsuploc  8094  suprleubex  8975  dfinfre  8977  zextlt  9412  prime  9419  infregelbex  9666  fzshftral  10177  nninfinf  10517  fimaxq  10901  clim  11427  clim2  11429  clim2c  11430  clim0c  11432  climabs0  11453  climrecvg1n  11494  mertenslem2  11682  mertensabs  11683  dfgcd2  12154  sqrt2irr  12303  pc11  12472  pcz  12473  1arith  12508  infpn2  12616  grpidpropdg  12960  sgrppropd  12999  mndpropd  13024  grppropd  13092  issubg4m  13266  rngpropd  13454  ringpropd  13537  oppr1g  13581  lsspropdg  13930  isridlrng  13981  isridl  14003  expghmap  14106  tgss2  14258  neipsm  14333  ssidcn  14389  lmbrf  14394  cnnei  14411  cnrest2  14415  lmss  14425  lmres  14427  ismet2  14533  elmopn2  14628  metss  14673  metrest  14685  metcnp  14691  metcnp2  14692  metcn  14693  txmetcnp  14697  divcnap  14744  elcncf2  14753  mulc1cncf  14768  cncfmet  14771  cdivcncfap  14783  limcdifap  14841  limcmpted  14842  cnlimc  14851  2sqlem6  15277  iswomni0  15611  cndcap  15619