Theorem ralbidva 2526

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

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

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  raleqbidva  2746  poinxp  4788  funimass4  5686  fnmptfvd  5741  funimass3  5753  funconstss  5755  cocan1  5917  cocan2  5918  isocnv2  5942  isores2  5943  isoini2  5949  ofrfval  6233  ofrfval2  6241  dfsmo2  6439  smores  6444  smores2  6446  ac6sfi  7068  supisolem  7186  ordiso2  7213  ismkvnex  7333  nninfwlporlemd  7350  caucvgsrlemcau  7991  suplocsrlempr  8005  axsuploc  8230  suprleubex  9112  dfinfre  9114  zextlt  9550  prime  9557  infregelbex  9805  fzshftral  10316  nninfinf  10677  fimaxq  11062  swrdspsleq  11215  pfxeq  11244  clim  11808  clim2  11810  clim2c  11811  clim0c  11813  climabs0  11834  climrecvg1n  11875  mertenslem2  12063  mertensabs  12064  dfgcd2  12551  sqrt2irr  12700  pc11  12870  pcz  12871  1arith  12906  infpn2  13043  grpidpropdg  13423  sgrppropd  13462  mndpropd  13489  grppropd  13566  issubg4m  13746  rngpropd  13934  ringpropd  14017  oppr1g  14061  lsspropdg  14411  isridlrng  14462  isridl  14484  expghmap  14587  tgss2  14769  neipsm  14844  ssidcn  14900  lmbrf  14905  cnnei  14922  cnrest2  14926  lmss  14936  lmres  14938  ismet2  15044  elmopn2  15139  metss  15184  metrest  15196  metcnp  15202  metcnp2  15203  metcn  15204  txmetcnp  15208  divcnap  15255  elcncf2  15264  mulc1cncf  15279  cncfmet  15282  cdivcncfap  15294  limcdifap  15352  limcmpted  15353  cnlimc  15362  mpodvdsmulf1o  15680  2sqlem6  15815  upgriswlkdc  16106  iswomni0  16507  cndcap  16515