Theorem rexbidva 2503

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

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

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-rex 2490

This theorem is referenced by:  2rexbiia  2522  2rexbidva  2529  rexeqbidva  2721  dfimafn  5627  funimass4  5629  fconstfvm  5802  fliftel  5862  fliftf  5868  f1oiso  5895  releldm2  6271  frecabcl  6485  qsinxp  6698  qliftel  6702  supisolem  7110  enumctlemm  7216  ismkvnex  7257  genpassl  7637  genpassu  7638  addcomprg  7691  mulcomprg  7693  1idprl  7703  1idpru  7704  archrecnq  7776  archrecpr  7777  caucvgprprlemexbt  7819  caucvgprprlemexb  7820  archsr  7895  map2psrprg  7918  suplocsrlempr  7920  axsuploc  8145  cnegexlem3  8249  cnegex2  8251  recexre  8651  rerecclap  8803  creur  9032  creui  9033  nndiv  9077  arch  9292  nnrecl  9293  expnlbnd  10809  fimaxq  10972  wrdval  10997  clim2  11594  clim2c  11595  clim0c  11597  climabs0  11618  climrecvg1n  11659  sumeq2  11670  mertensabs  11848  prodeq2  11868  zproddc  11890  nndivides  12108  alzdvds  12165  oddm1even  12186  oddnn02np1  12191  oddge22np1  12192  evennn02n  12193  evennn2n  12194  divalgb  12236  modremain  12240  modprmn0modprm0  12579  pythagtriplem2  12589  pythagtrip  12606  pceu  12618  4sqlem12  12725  gsumpropd2  13225  mndpfo  13270  mndpropd  13272  grppropd  13349  conjnmzb  13616  dvdsr02  13867  crngunit  13873  dvdsrpropdg  13909  cnfldui  14351  znunit  14421  iscnp3  14675  lmbrf  14687  cncnp  14702  lmss  14718  metrest  14978  metcnp  14984  metcnp2  14985  txmetcnp  14990  cdivcncfap  15076  ivthdec  15116  lgsquadlem2  15555  2lgslem1a  15565  pw1nct  15940