Theorem rexbidva 2547

Description: Formula-building rule for restricted existential quantifier (deduction form). (Contributed by NM, 9-Mar-1997.)

Hypothesis

Ref	Expression
ralbidva.1	|- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )

Assertion

Ref	Expression
rexbidva	|- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

Distinct variable group:   ph, x

Allowed substitution hints:   ps( x)   ch( x)   A( x)

Proof of Theorem rexbidva

Step	Hyp	Ref	Expression
1		nfv 1581	. 2 |- F/ x ph
2		ralbidva.1	. 2 |- ( ( ph /\ x e. A ) -> ( ps <-> ch ) )
3	1, 2	rexbida 2545	1 |- ( ph -> ( E. x e. A ps <-> E. x e. A ch ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2209   E.wrex 2529

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-ie1 1546  ax-ie2 1547  ax-4 1563  ax-17 1579  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-rex 2534

This theorem is used by:  2rexbiia  2566  2rexbidva  2573  rexeqbidva  2768  dfimafn  5751  funimass4  5753  fconstfvm  5933  dfimafnf  5955  fliftel  5999  fliftf  6005  f1oiso  6032  releldm2  6419  frecabcl  6670  qsinxp  6885  qliftel  6889  supisolem  7349  enumctlemm  7455  ismkvnex  7496  genpassl  7892  genpassu  7893  addcomprg  7946  mulcomprg  7948  1idprl  7958  1idpru  7959  archrecnq  8031  archrecpr  8032  caucvgprprlemexbt  8074  caucvgprprlemexb  8075  archsr  8150  map2psrprg  8173  suplocsrlempr  8175  axsuploc  8399  cnegexlem3  8505  cnegex2  8507  recexre  8909  rerecclap  9063  creur  9292  creui  9293  nndiv  9348  arch  9565  nnrecl  9566  expnlbnd  11117  nn0sqdc  11162  fimaxq  11286  wrdval  11323  clim2  12068  clim2c  12069  clim0c  12071  climabs0  12092  climrecvg1n  12133  sumeq2  12144  mertensabs  12323  prodeq2  12343  zproddc  12365  nndivides  12583  alzdvds  12640  oddm1even  12661  oddnn02np1  12666  oddge22np1  12667  evennn02n  12668  evennn2n  12669  divalgb  12711  modremain  12715  modprmn0modprm0  13058  pythagtriplem2  13068  pythagtrip  13085  pceu  13097  4sqlem12  13204  ballotfilemsima  13311  mndpfo  13804  mndpropd  13806  grppropd  13875  conjnmzb  14136  dvdsr02  14496  crngunit  14502  dvdsrpropdg  14538  cnfldui  15008  znunit  15078  iscnp3  15395  lmbrf  15407  cncnp  15422  lmss  15438  metrest  15698  metcnp  15704  metcnp2  15705  txmetcnp  15710  cdivcncfap  15796  ivthdec  15836  bpos  16281  lgsquadlem2  16363  2lgslem1a  16373  pw1nct  17199