Theorem rexbidva 2494

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-rex 2481

This theorem is referenced by:  2rexbiia  2513  2rexbidva  2520  rexeqbidva  2712  dfimafn  5609  funimass4  5611  fconstfvm  5780  fliftel  5840  fliftf  5846  f1oiso  5873  releldm2  6243  frecabcl  6457  qsinxp  6670  qliftel  6674  supisolem  7074  enumctlemm  7180  ismkvnex  7221  genpassl  7591  genpassu  7592  addcomprg  7645  mulcomprg  7647  1idprl  7657  1idpru  7658  archrecnq  7730  archrecpr  7731  caucvgprprlemexbt  7773  caucvgprprlemexb  7774  archsr  7849  map2psrprg  7872  suplocsrlempr  7874  axsuploc  8099  cnegexlem3  8203  cnegex2  8205  recexre  8605  rerecclap  8757  creur  8986  creui  8987  nndiv  9031  arch  9246  nnrecl  9247  expnlbnd  10756  fimaxq  10919  wrdval  10938  clim2  11448  clim2c  11449  clim0c  11451  climabs0  11472  climrecvg1n  11513  sumeq2  11524  mertensabs  11702  prodeq2  11722  zproddc  11744  nndivides  11962  alzdvds  12019  oddm1even  12040  oddnn02np1  12045  oddge22np1  12046  evennn02n  12047  evennn2n  12048  divalgb  12090  modremain  12094  modprmn0modprm0  12425  pythagtriplem2  12435  pythagtrip  12452  pceu  12464  4sqlem12  12571  gsumpropd2  13036  mndpfo  13079  mndpropd  13081  grppropd  13149  conjnmzb  13410  dvdsr02  13661  crngunit  13667  dvdsrpropdg  13703  cnfldui  14145  znunit  14215  iscnp3  14439  lmbrf  14451  cncnp  14466  lmss  14482  metrest  14742  metcnp  14748  metcnp2  14749  txmetcnp  14754  cdivcncfap  14840  ivthdec  14880  lgsquadlem2  15319  2lgslem1a  15329  pw1nct  15647