Theorem rexbidva 2378

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473

This theorem depends on definitions:  df-bi 116  df-nf 1396  df-rex 2366

This theorem is referenced by:  2rexbiia  2395  2rexbidva  2402  rexeqbidva  2578  dfimafn  5366  funimass4  5368  fconstfvm  5529  fliftel  5586  fliftf  5592  f1oiso  5619  releldm2  5969  frecabcl  6178  qsinxp  6382  qliftel  6386  supisolem  6757  enumctlemm  6846  genpassl  7144  genpassu  7145  addcomprg  7198  mulcomprg  7200  1idprl  7210  1idpru  7211  archrecnq  7283  archrecpr  7284  caucvgprprlemexbt  7326  caucvgprprlemexb  7327  archsr  7388  cnegexlem3  7720  cnegex2  7722  recexre  8116  rerecclap  8258  creur  8480  creui  8481  nndiv  8524  arch  8731  nnrecl  8732  expnlbnd  10139  fimaxq  10296  clim2  10732  clim2c  10733  clim0c  10735  climabs0  10757  climrecvg1n  10798  sumeq2  10809  mertensabs  10992  nndivides  11142  alzdvds  11194  oddm1even  11214  oddnn02np1  11219  oddge22np1  11220  evennn02n  11221  evennn2n  11222  divalgb  11264  modremain  11268