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  4728  funimass4  5607  fnmptfvd  5662  funimass3  5674  funconstss  5676  cocan1  5830  cocan2  5831  isocnv2  5855  isores2  5856  isoini2  5862  ofrfval  6139  ofrfval2  6147  dfsmo2  6340  smores  6345  smores2  6347  ac6sfi  6954  supisolem  7067  ordiso2  7094  ismkvnex  7214  nninfwlporlemd  7231  caucvgsrlemcau  7853  suplocsrlempr  7867  axsuploc  8092  suprleubex  8973  dfinfre  8975  zextlt  9409  prime  9416  infregelbex  9663  fzshftral  10174  nninfinf  10514  fimaxq  10898  clim  11424  clim2  11426  clim2c  11427  clim0c  11429  climabs0  11450  climrecvg1n  11491  mertenslem2  11679  mertensabs  11680  dfgcd2  12151  sqrt2irr  12300  pc11  12469  pcz  12470  1arith  12505  infpn2  12613  grpidpropdg  12957  sgrppropd  12996  mndpropd  13021  grppropd  13089  issubg4m  13263  rngpropd  13451  ringpropd  13534  oppr1g  13578  lsspropdg  13927  isridlrng  13978  isridl  14000  expghmap  14095  tgss2  14247  neipsm  14322  ssidcn  14378  lmbrf  14383  cnnei  14400  cnrest2  14404  lmss  14414  lmres  14416  ismet2  14522  elmopn2  14617  metss  14662  metrest  14674  metcnp  14680  metcnp2  14681  metcn  14682  txmetcnp  14686  divcnap  14723  elcncf2  14729  mulc1cncf  14744  cncfmet  14747  cdivcncfap  14758  limcdifap  14816  limcmpted  14817  cnlimc  14826  2sqlem6  15207  iswomni0  15541  cndcap  15549