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  4793  funimass4  5692  fnmptfvd  5747  funimass3  5759  funconstss  5761  cocan1  5923  cocan2  5924  isocnv2  5948  isores2  5949  isoini2  5955  ofrfval  6239  ofrfval2  6247  dfsmo2  6448  smores  6453  smores2  6455  ac6sfi  7080  supisolem  7198  ordiso2  7225  ismkvnex  7345  nninfwlporlemd  7362  caucvgsrlemcau  8003  suplocsrlempr  8017  axsuploc  8242  suprleubex  9124  dfinfre  9126  zextlt  9562  prime  9569  infregelbex  9822  fzshftral  10333  nninfinf  10695  fimaxq  11081  swrdspsleq  11238  pfxeq  11267  clim  11832  clim2  11834  clim2c  11835  clim0c  11837  climabs0  11858  climrecvg1n  11899  mertenslem2  12087  mertensabs  12088  dfgcd2  12575  sqrt2irr  12724  pc11  12894  pcz  12895  1arith  12930  infpn2  13067  grpidpropdg  13447  sgrppropd  13486  mndpropd  13513  grppropd  13590  issubg4m  13770  rngpropd  13958  ringpropd  14041  oppr1g  14085  lsspropdg  14435  isridlrng  14486  isridl  14508  expghmap  14611  tgss2  14793  neipsm  14868  ssidcn  14924  lmbrf  14929  cnnei  14946  cnrest2  14950  lmss  14960  lmres  14962  ismet2  15068  elmopn2  15163  metss  15208  metrest  15220  metcnp  15226  metcnp2  15227  metcn  15228  txmetcnp  15232  divcnap  15279  elcncf2  15288  mulc1cncf  15303  cncfmet  15306  cdivcncfap  15318  limcdifap  15376  limcmpted  15377  cnlimc  15386  mpodvdsmulf1o  15704  2sqlem6  15839  upgriswlkdc  16157  clwwlknonex2lem2  16233  iswomni0  16591  cndcap  16599