Theorem ralbidva 2540

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

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

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-ral 2527

This theorem is referenced by:  raleqbidva  2761  poinxp  4824  funimass4  5732  fnmptfvd  5787  funimass3  5799  funconstss  5801  cocan1  5966  cocan2  5967  isocnv2  5991  isores2  5992  isoini2  5998  ofrfval  6284  ofrfval2  6292  dfsmo2  6531  smores  6536  smores2  6538  ac6sfi  7168  supisolem  7312  ordiso2  7339  ismkvnex  7459  nninfwlporlemd  7476  caucvgsrlemcau  8124  suplocsrlempr  8138  axsuploc  8362  suprleubex  9245  dfinfre  9247  zextlt  9688  prime  9695  infregelbex  9948  fzshftral  10464  nninfinf  10829  fimaxq  11219  swrdspsleq  11384  pfxeq  11413  clim  11991  clim2  11993  clim2c  11994  clim0c  11996  climabs0  12017  climrecvg1n  12058  mertenslem2  12247  mertensabs  12248  dfgcd2  12735  sqrt2irr  12884  pc11  13054  pcz  13055  1arith  13090  ballotfilemodife  13184  infpn2  13291  grpidpropdg  13637  sgrppropd  13676  mndpropd  13701  grppropd  13772  issubg4m  13946  rngpropd  14194  ringpropd  14281  oppr1g  14326  opprdrng  14558  lsspropdg  14705  isridlrng  14756  isridl  14778  expghmap  14881  psrbagconf1o  14954  tgss2  15070  neipsm  15145  ssidcn  15201  lmbrf  15206  cnnei  15223  cnrest2  15227  lmss  15237  lmres  15239  ismet2  15345  elmopn2  15440  metss  15485  metrest  15497  metcnp  15503  metcnp2  15504  metcn  15505  txmetcnp  15509  divcnap  15556  elcncf2  15565  mulc1cncf  15580  cncfmet  15583  cdivcncfap  15595  limcdifap  15653  limcmpted  15654  cnlimc  15663  mpodvdsmulf1o  15984  2sqlem6  16119  upgriswlkdc  16481  clwwlknonex2lem2  16559  iswomni0  16962  cndcap  16970