Theorem ralbidva 2528

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

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

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  raleqbidva  2748  poinxp  4795  funimass4  5696  fnmptfvd  5751  funimass3  5763  funconstss  5765  cocan1  5927  cocan2  5928  isocnv2  5952  isores2  5953  isoini2  5959  ofrfval  6243  ofrfval2  6251  dfsmo2  6452  smores  6457  smores2  6459  ac6sfi  7086  supisolem  7206  ordiso2  7233  ismkvnex  7353  nninfwlporlemd  7370  caucvgsrlemcau  8012  suplocsrlempr  8026  axsuploc  8251  suprleubex  9133  dfinfre  9135  zextlt  9571  prime  9578  infregelbex  9831  fzshftral  10342  nninfinf  10704  fimaxq  11090  swrdspsleq  11247  pfxeq  11276  clim  11841  clim2  11843  clim2c  11844  clim0c  11846  climabs0  11867  climrecvg1n  11908  mertenslem2  12096  mertensabs  12097  dfgcd2  12584  sqrt2irr  12733  pc11  12903  pcz  12904  1arith  12939  infpn2  13076  grpidpropdg  13456  sgrppropd  13495  mndpropd  13522  grppropd  13599  issubg4m  13779  rngpropd  13967  ringpropd  14050  oppr1g  14094  lsspropdg  14444  isridlrng  14495  isridl  14517  expghmap  14620  tgss2  14802  neipsm  14877  ssidcn  14933  lmbrf  14938  cnnei  14955  cnrest2  14959  lmss  14969  lmres  14971  ismet2  15077  elmopn2  15172  metss  15217  metrest  15229  metcnp  15235  metcnp2  15236  metcn  15237  txmetcnp  15241  divcnap  15288  elcncf2  15297  mulc1cncf  15312  cncfmet  15315  cdivcncfap  15327  limcdifap  15385  limcmpted  15386  cnlimc  15395  mpodvdsmulf1o  15713  2sqlem6  15848  upgriswlkdc  16210  clwwlknonex2lem2  16288  iswomni0  16655  cndcap  16663