Theorem ralbidva 2493

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

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

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  raleqbidva  2711  poinxp  4733  funimass4  5614  fnmptfvd  5669  funimass3  5681  funconstss  5683  cocan1  5837  cocan2  5838  isocnv2  5862  isores2  5863  isoini2  5869  ofrfval  6148  ofrfval2  6156  dfsmo2  6354  smores  6359  smores2  6361  ac6sfi  6968  supisolem  7083  ordiso2  7110  ismkvnex  7230  nninfwlporlemd  7247  caucvgsrlemcau  7879  suplocsrlempr  7893  axsuploc  8118  suprleubex  9000  dfinfre  9002  zextlt  9437  prime  9444  infregelbex  9691  fzshftral  10202  nninfinf  10554  fimaxq  10938  clim  11465  clim2  11467  clim2c  11468  clim0c  11470  climabs0  11491  climrecvg1n  11532  mertenslem2  11720  mertensabs  11721  dfgcd2  12208  sqrt2irr  12357  pc11  12527  pcz  12528  1arith  12563  infpn2  12700  grpidpropdg  13078  sgrppropd  13117  mndpropd  13144  grppropd  13221  issubg4m  13401  rngpropd  13589  ringpropd  13672  oppr1g  13716  lsspropdg  14065  isridlrng  14116  isridl  14138  expghmap  14241  tgss2  14423  neipsm  14498  ssidcn  14554  lmbrf  14559  cnnei  14576  cnrest2  14580  lmss  14590  lmres  14592  ismet2  14698  elmopn2  14793  metss  14838  metrest  14850  metcnp  14856  metcnp2  14857  metcn  14858  txmetcnp  14862  divcnap  14909  elcncf2  14918  mulc1cncf  14933  cncfmet  14936  cdivcncfap  14948  limcdifap  15006  limcmpted  15007  cnlimc  15016  mpodvdsmulf1o  15334  2sqlem6  15469  iswomni0  15808  cndcap  15816