Theorem ralbidva 2546

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

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2209   A.wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  raleqbidva  2767  poinxp  4844  funimass4  5753  fnmptfvd  5813  funimass3  5825  funconstss  5827  cocan1  5993  cocan2  5994  isocnv2  6018  isores2  6019  isoini2  6025  ofrfval  6311  ofrfval2  6319  dfsmo2  6558  smores  6563  smores2  6565  ac6sfi  7202  supisolem  7348  ordiso2  7375  ismkvnex  7495  nninfwlporlemd  7512  caucvgsrlemcau  8160  suplocsrlempr  8174  axsuploc  8398  suprleubex  9286  dfinfre  9288  zextlt  9742  prime  9749  infregelbex  10007  fzshftral  10525  nninfinf  10893  fimaxq  11284  swrdspsleq  11453  pfxeq  11482  clim  12063  clim2  12065  clim2c  12066  clim0c  12068  climabs0  12089  climrecvg1n  12130  mertenslem2  12319  mertensabs  12320  dfgcd2  12807  sqrt2irr  12957  pc11  13130  pcz  13131  1arith  13166  ballotfilemodife  13289  infpn2  13396  grpidpropdg  13743  sgrppropd  13777  mndpropd  13802  grppropd  13871  issubg4m  14045  rngpropd  14303  ringpropd  14392  oppr1g  14437  opprdrng  14669  lsspropdg  14817  isridlrng  14868  isridl  14890  expghmap  14991  assapropd  15063  psrbagconf1o  15113  tgss2  15229  neipsm  15304  ssidcn  15360  lmbrf  15365  cnnei  15382  cnrest2  15386  lmss  15396  lmres  15398  ismet2  15504  elmopn2  15599  metss  15644  metrest  15656  metcnp  15662  metcnp2  15663  metcn  15664  txmetcnp  15668  divcnap  15715  elcncf2  15724  mulc1cncf  15739  cncfmet  15742  cdivcncfap  15754  limcdifap  15812  limcmpted  15813  cnlimc  15822  mpodvdsmulf1o  16185  2sqlem6  16337  upgriswlkdc  16699  clwwlknonex2lem2  16777  iswomni0  17199  cndcap  17207