Theorem rexbidva 2529

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

Syntax hints:   -> wi 4   /\ wa 104   <-> wb 105   e. wcel 2202   E.wrex 2511

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-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-rex 2516

This theorem is referenced by:  2rexbiia  2548  2rexbidva  2555  rexeqbidva  2749  dfimafn  5694  funimass4  5696  fconstfvm  5872  fliftel  5934  fliftf  5940  f1oiso  5967  releldm2  6348  frecabcl  6565  qsinxp  6780  qliftel  6784  supisolem  7207  enumctlemm  7313  ismkvnex  7354  genpassl  7744  genpassu  7745  addcomprg  7798  mulcomprg  7800  1idprl  7810  1idpru  7811  archrecnq  7883  archrecpr  7884  caucvgprprlemexbt  7926  caucvgprprlemexb  7927  archsr  8002  map2psrprg  8025  suplocsrlempr  8027  axsuploc  8252  cnegexlem3  8356  cnegex2  8358  recexre  8758  rerecclap  8910  creur  9139  creui  9140  nndiv  9184  arch  9399  nnrecl  9400  expnlbnd  10927  fimaxq  11092  wrdval  11120  clim2  11861  clim2c  11862  clim0c  11864  climabs0  11885  climrecvg1n  11926  sumeq2  11937  mertensabs  12116  prodeq2  12136  zproddc  12158  nndivides  12376  alzdvds  12433  oddm1even  12454  oddnn02np1  12459  oddge22np1  12460  evennn02n  12461  evennn2n  12462  divalgb  12504  modremain  12508  modprmn0modprm0  12847  pythagtriplem2  12857  pythagtrip  12874  pceu  12886  4sqlem12  12993  gsumpropd2  13494  mndpfo  13539  mndpropd  13541  grppropd  13618  conjnmzb  13885  dvdsr02  14138  crngunit  14144  dvdsrpropdg  14180  cnfldui  14622  znunit  14692  iscnp3  14946  lmbrf  14958  cncnp  14973  lmss  14989  metrest  15249  metcnp  15255  metcnp2  15256  txmetcnp  15261  cdivcncfap  15347  ivthdec  15387  lgsquadlem2  15826  2lgslem1a  15836  pw1nct  16655