Theorem rexbidva 2454

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

Syntax hints:   -> wi 4   /\ wa 103   <-> wb 104   e. wcel 2128   E.wrex 2436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-rex 2441

This theorem is referenced by:  2rexbiia  2473  2rexbidva  2480  rexeqbidva  2667  dfimafn  5519  funimass4  5521  fconstfvm  5687  fliftel  5745  fliftf  5751  f1oiso  5778  releldm2  6135  frecabcl  6348  qsinxp  6558  qliftel  6562  supisolem  6954  enumctlemm  7060  ismkvnex  7100  genpassl  7446  genpassu  7447  addcomprg  7500  mulcomprg  7502  1idprl  7512  1idpru  7513  archrecnq  7585  archrecpr  7586  caucvgprprlemexbt  7628  caucvgprprlemexb  7629  archsr  7704  map2psrprg  7727  suplocsrlempr  7729  axsuploc  7952  cnegexlem3  8056  cnegex2  8058  recexre  8457  rerecclap  8607  creur  8835  creui  8836  nndiv  8879  arch  9092  nnrecl  9093  expnlbnd  10551  fimaxq  10712  clim2  11191  clim2c  11192  clim0c  11194  climabs0  11215  climrecvg1n  11256  sumeq2  11267  mertensabs  11445  prodeq2  11465  zproddc  11487  nndivides  11704  alzdvds  11758  oddm1even  11778  oddnn02np1  11783  oddge22np1  11784  evennn02n  11785  evennn2n  11786  divalgb  11828  modremain  11832  modprmn0modprm0  12146  pythagtriplem2  12156  pythagtrip  12173  pceu  12185  iscnp3  12673  lmbrf  12685  cncnp  12700  lmss  12716  metrest  12976  metcnp  12982  metcnp2  12983  txmetcnp  12988  cdivcncfap  13057  ivthdec  13092  pw1nct  13646