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  5605  funimass4  5607  fconstfvm  5776  fliftel  5836  fliftf  5842  f1oiso  5869  releldm2  6238  frecabcl  6452  qsinxp  6665  qliftel  6669  supisolem  7067  enumctlemm  7173  ismkvnex  7214  genpassl  7584  genpassu  7585  addcomprg  7638  mulcomprg  7640  1idprl  7650  1idpru  7651  archrecnq  7723  archrecpr  7724  caucvgprprlemexbt  7766  caucvgprprlemexb  7767  archsr  7842  map2psrprg  7865  suplocsrlempr  7867  axsuploc  8092  cnegexlem3  8196  cnegex2  8198  recexre  8597  rerecclap  8749  creur  8978  creui  8979  nndiv  9023  arch  9237  nnrecl  9238  expnlbnd  10735  fimaxq  10898  wrdval  10917  clim2  11426  clim2c  11427  clim0c  11429  climabs0  11450  climrecvg1n  11491  sumeq2  11502  mertensabs  11680  prodeq2  11700  zproddc  11722  nndivides  11940  alzdvds  11996  oddm1even  12016  oddnn02np1  12021  oddge22np1  12022  evennn02n  12023  evennn2n  12024  divalgb  12066  modremain  12070  modprmn0modprm0  12394  pythagtriplem2  12404  pythagtrip  12421  pceu  12433  4sqlem12  12540  gsumpropd2  12976  mndpfo  13019  mndpropd  13021  grppropd  13089  conjnmzb  13350  dvdsr02  13601  crngunit  13607  dvdsrpropdg  13643  cnfldui  14077  znunit  14147  iscnp3  14371  lmbrf  14383  cncnp  14398  lmss  14414  metrest  14674  metcnp  14680  metcnp2  14681  txmetcnp  14686  cdivcncfap  14758  ivthdec  14798  pw1nct  15493