Theorem rexbidva 2491

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

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

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-rex 2478

This theorem is referenced by:  2rexbiia  2510  2rexbidva  2517  rexeqbidva  2709  dfimafn  5606  funimass4  5608  fconstfvm  5777  fliftel  5837  fliftf  5843  f1oiso  5870  releldm2  6240  frecabcl  6454  qsinxp  6667  qliftel  6671  supisolem  7069  enumctlemm  7175  ismkvnex  7216  genpassl  7586  genpassu  7587  addcomprg  7640  mulcomprg  7642  1idprl  7652  1idpru  7653  archrecnq  7725  archrecpr  7726  caucvgprprlemexbt  7768  caucvgprprlemexb  7769  archsr  7844  map2psrprg  7867  suplocsrlempr  7869  axsuploc  8094  cnegexlem3  8198  cnegex2  8200  recexre  8599  rerecclap  8751  creur  8980  creui  8981  nndiv  9025  arch  9240  nnrecl  9241  expnlbnd  10738  fimaxq  10901  wrdval  10920  clim2  11429  clim2c  11430  clim0c  11432  climabs0  11453  climrecvg1n  11494  sumeq2  11505  mertensabs  11683  prodeq2  11703  zproddc  11725  nndivides  11943  alzdvds  11999  oddm1even  12019  oddnn02np1  12024  oddge22np1  12025  evennn02n  12026  evennn2n  12027  divalgb  12069  modremain  12073  modprmn0modprm0  12397  pythagtriplem2  12407  pythagtrip  12424  pceu  12436  4sqlem12  12543  gsumpropd2  12979  mndpfo  13022  mndpropd  13024  grppropd  13092  conjnmzb  13353  dvdsr02  13604  crngunit  13610  dvdsrpropdg  13646  cnfldui  14088  znunit  14158  iscnp3  14382  lmbrf  14394  cncnp  14409  lmss  14425  metrest  14685  metcnp  14691  metcnp2  14692  txmetcnp  14697  cdivcncfap  14783  ivthdec  14823  lgsquadlem2  15235  2lgslem1a  15245  pw1nct  15563