Theorem ralbidva 2493

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  raleqbidva  2711  poinxp  4733  funimass4  5614  fnmptfvd  5669  funimass3  5681  funconstss  5683  cocan1  5837  cocan2  5838  isocnv2  5862  isores2  5863  isoini2  5869  ofrfval  6148  ofrfval2  6156  dfsmo2  6354  smores  6359  smores2  6361  ac6sfi  6968  supisolem  7083  ordiso2  7110  ismkvnex  7230  nninfwlporlemd  7247  caucvgsrlemcau  7877  suplocsrlempr  7891  axsuploc  8116  suprleubex  8998  dfinfre  9000  zextlt  9435  prime  9442  infregelbex  9689  fzshftral  10200  nninfinf  10552  fimaxq  10936  clim  11463  clim2  11465  clim2c  11466  clim0c  11468  climabs0  11489  climrecvg1n  11530  mertenslem2  11718  mertensabs  11719  dfgcd2  12206  sqrt2irr  12355  pc11  12525  pcz  12526  1arith  12561  infpn2  12698  grpidpropdg  13076  sgrppropd  13115  mndpropd  13142  grppropd  13219  issubg4m  13399  rngpropd  13587  ringpropd  13670  oppr1g  13714  lsspropdg  14063  isridlrng  14114  isridl  14136  expghmap  14239  tgss2  14399  neipsm  14474  ssidcn  14530  lmbrf  14535  cnnei  14552  cnrest2  14556  lmss  14566  lmres  14568  ismet2  14674  elmopn2  14769  metss  14814  metrest  14826  metcnp  14832  metcnp2  14833  metcn  14834  txmetcnp  14838  divcnap  14885  elcncf2  14894  mulc1cncf  14909  cncfmet  14912  cdivcncfap  14924  limcdifap  14982  limcmpted  14983  cnlimc  14992  mpodvdsmulf1o  15310  2sqlem6  15445  iswomni0  15782  cndcap  15790