Theorem rexbidva 2474

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

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

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-rex 2461

This theorem is referenced by:  2rexbiia  2493  2rexbidva  2500  rexeqbidva  2687  dfimafn  5563  funimass4  5565  fconstfvm  5733  fliftel  5791  fliftf  5797  f1oiso  5824  releldm2  6183  frecabcl  6397  qsinxp  6608  qliftel  6612  supisolem  7004  enumctlemm  7110  ismkvnex  7150  genpassl  7520  genpassu  7521  addcomprg  7574  mulcomprg  7576  1idprl  7586  1idpru  7587  archrecnq  7659  archrecpr  7660  caucvgprprlemexbt  7702  caucvgprprlemexb  7703  archsr  7778  map2psrprg  7801  suplocsrlempr  7803  axsuploc  8026  cnegexlem3  8130  cnegex2  8132  recexre  8531  rerecclap  8683  creur  8912  creui  8913  nndiv  8956  arch  9169  nnrecl  9170  expnlbnd  10639  fimaxq  10800  clim2  11284  clim2c  11285  clim0c  11287  climabs0  11308  climrecvg1n  11349  sumeq2  11360  mertensabs  11538  prodeq2  11558  zproddc  11580  nndivides  11797  alzdvds  11852  oddm1even  11872  oddnn02np1  11877  oddge22np1  11878  evennn02n  11879  evennn2n  11880  divalgb  11922  modremain  11926  modprmn0modprm0  12248  pythagtriplem2  12258  pythagtrip  12275  pceu  12287  mndpfo  12771  mndpropd  12773  grppropd  12825  dvdsr02  13205  crngunit  13211  dvdsrpropdg  13247  iscnp3  13574  lmbrf  13586  cncnp  13601  lmss  13617  metrest  13877  metcnp  13883  metcnp2  13884  txmetcnp  13889  cdivcncfap  13958  ivthdec  13993  pw1nct  14612